chore: bump to v4.28.0 (#536)

Author: Ruben-VandeVelde

Carleson/Antichain/AntichainOperator.lean

@@ -154,7 +154,7 @@ lemma eLpNorm_le_M14 {p : 𝔓 X} (mp : p ∈ 𝔄) {x₀ : X} (hx : x₀ ∈ ba
   · exact Or.inl <| (by finiteness)
   rw [ENNReal.div_eq_inv_mul, ← ENNReal.rpow_neg_one, ← ENNReal.rpow_mul, mul_comm _ (-1),
     ENNReal.rpow_mul, ENNReal.rpow_neg_one,
-    eLpNorm_eq_lintegral_rpow_enorm (by simpa) (by finiteness)]
+    eLpNorm_eq_lintegral_rpow_enorm_toReal (by simpa) (by finiteness)]
   simp_rw [ENNReal.toReal_ofReal hr.le, one_div]
   rw [← ENNReal.mul_rpow_of_nonneg _ _ (by positivity), M14, maximalFunction]
   refine ENNReal.rpow_le_rpow ?_ (by positivity)

Carleson/Antichain/Basic.lean

@@ -327,7 +327,7 @@ lemma eLpNorm_𝓜_le_eLpNorm_𝓜p_mul (hf : Measurable f) (hfF : ∀ x, ‖f x
       ring
     _ ≤ _ := by
       gcongr
-      · rw [eLpNorm_eq_lintegral_rpow_enorm (by assumption) (by assumption), toReal_ofReal <|
+      · rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by assumption) (by assumption), toReal_ofReal <|
           le_of_lt p'_pos, one_div, ← div_rpow_of_nonneg _ _ (le_of_lt inv_p'_pos), dens₂]
         gcongr
         refine le_trans ?_ <| le_iSup₂ 𝔭 h𝔭
@@ -343,7 +343,7 @@ lemma eLpNorm_𝓜_le_eLpNorm_𝓜p_mul (hf : Measurable f) (hfF : ∀ x, ‖f x
           rw [Pi.one_apply, mul_one, enorm_indicator_eq_indicator_enorm, indicator, indicator]
           split_ifs <;> simp [p'_pos]
         · exact Measure.restrict_apply_univ B
-      · rw [eLpNorm_eq_lintegral_rpow_enorm (by assumption) (by assumption),
+      · rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by assumption) (by assumption),
           toReal_ofReal <| le_of_lt p_pos, 𝓜p, maximalFunction, one_div,
           ← div_rpow_of_nonneg _ _ (le_of_lt inv_p_pos), ← laverage_eq, hp_coe]
         gcongr

Carleson/Classical/VanDerCorput.lean

@@ -36,7 +36,7 @@ lemma intervalIntegrable_continuous_mul_lipschitzOnWith
       rw [Real.Ioo_eq_ball] at hy
       simp only [Metric.mem_ball, dist_eq_norm] at hy
       exact hy.le
-  apply (hf.continuousOn.mul hg.continuousOn).intervalIntegrable_Ioo_of_bound hab
+  apply (hf.continuousOn.fun_mul hg.continuousOn).intervalIntegrable_Ioo_of_bound hab
     (C := C * D) (fun x hx ↦ ?_)
   rw [norm_mul, mul_comm, mul_comm C]
   gcongr

Carleson/ForestOperator/RemainingTiles.lean

@@ -327,17 +327,17 @@ lemma square_function_count (hJ : J ∈ 𝓙₆ t u₁) {s' : ℤ} :
       intro I
       simp_rw [Finset.filter_filter, Finset.mem_filter_univ, mem_toFinset]
       exact fun H ↦ ⟨H.2, H.1.1⟩
-    · have (I : Grid X) : ball (c I) (8 * D ^ s I) = EMetric.ball (c I) (8 * D ^ s I) := by
-        trans EMetric.ball (c I) (show ℝ≥0 from ⟨8 * D ^ s I, by positivity⟩)
-        · rw [emetric_ball_nnreal]; rfl
+    · have (I : Grid X) : ball (c I) (8 * D ^ s I) = Metric.eball (c I) (8 * D ^ s I) := by
+        trans Metric.eball (c I) (show ℝ≥0 from ⟨8 * D ^ s I, by positivity⟩)
+        · rw [Metric.eball_coe]; rfl
         · congr!
           simp only [ENNReal.coe_nnreal_eq, ← Real.rpow_intCast]
           erw [ENNReal.ofReal_mul (by norm_num)]
           rw [← ENNReal.ofReal_rpow_of_pos (by simp), ENNReal.ofReal_natCast]
           norm_num
       simp_rw [this]
       simp only [CharP.cast_eq_zero, nonpos_iff_eq_zero, Finset.sum_eq_zero_iff, Finset.mem_filter,
-        Finset.mem_univ, true_and, indicator_apply_eq_zero, EMetric.mem_ball, Pi.one_apply,
+        Finset.mem_univ, true_and, indicator_apply_eq_zero, Metric.mem_eball, Pi.one_apply,
         one_ne_zero, imp_false, not_lt, and_imp]
       intro I e hI₁ _
       simp only [Grid.mem_def, mem_setOf_eq, not_and, not_le, supp, ← e] at hx'
@@ -388,7 +388,7 @@ lemma btp_expansion (hf : BoundedCompactSupport f) :
     _ = (∫⁻ x, ∑ J ∈ (𝓙₆ t u₁).toFinset, (J : Set X).indicator (fun _ ↦
         ‖⨍ y in J, ‖adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f y‖‖ₑ ^ 2) x) ^ (2 : ℝ)⁻¹ := by
       unfold approxOnCube
-      simp_rw [eLpNorm_eq_lintegral_rpow_enorm two_ne_zero ENNReal.ofNat_ne_top,
+      simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal two_ne_zero ENNReal.ofNat_ne_top,
         ENNReal.toReal_ofNat, one_div]
       congr! with x; rw [ENNReal.enorm_sum_eq_sum_enorm]; swap
       · refine fun J mJ ↦ indicator_nonneg (fun y my ↦ ?_) _
@@ -682,8 +682,9 @@ lemma e764_postCS (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
       congr; rw [← lintegral_biUnion_finset _ fun _ _ ↦ coeGrid_measurable]; swap
       · rw [coe_toFinset]; exact pairwiseDisjoint_𝓙₆
       simp_rw [mem_toFinset, union_𝓙₆ hu₁, ← lintegral_indicator coeGrid_measurable,
-        eLpNorm_eq_lintegral_rpow_enorm two_ne_zero ENNReal.ofNat_ne_top, ENNReal.toReal_ofNat,
-        one_div, show (2 : ℝ) = (2 : ℕ) by rfl, ENNReal.rpow_natCast, enorm_eq_self]
+        eLpNorm_eq_lintegral_rpow_enorm_toReal two_ne_zero ENNReal.ofNat_ne_top,
+        ENNReal.toReal_ofNat, one_div, show (2 : ℝ) = (2 : ℕ) by rfl, ENNReal.rpow_natCast,
+        enorm_eq_self]
       congr! with x
       simp_rw [sq, ← inter_indicator_mul, inter_self]
 

Carleson/TileExistence.lean

@@ -824,7 +824,7 @@ lemma transitive_boundary' {k1 k2 k3 : ℤ} (hk1 : -S ≤ k1) (hk2 : -S ≤ k2)
   · apply lt_of_le_of_lt (Metric.infEDist_anti _) hx'
     rw [compl_subset_compl]
     exact hi3_2_3
-  · rw [← emetric_ball,EMetric.mem_ball] at hx_4k2 hx_4k2'
+  · rw [← eball_ofReal, Metric.mem_eball] at hx_4k2 hx_4k2'
     rw [edist_comm] at hx_4k2'
     rw [← Real.rpow_intCast] at hx_4k2 hx_4k2'
     rw [ENNReal.ofReal_mul (by norm_num), ← ENNReal.ofReal_rpow_of_pos (realD_pos a),
@@ -1405,7 +1405,7 @@ lemma boundary_measure {k : ℤ} (hk : -S ≤ k) (y : Yk X k) {t : ℝ≥0} (ht
       · apply dyadic_property hconst_n hconst_n_k hk y y'
         rw [not_disjoint_iff]
         use x
-      rw [← emetric_ball, EMetric.mem_ball,ENNReal.ofReal_mul (by norm_num), ENNReal.ofReal_ofNat,
+      rw [← eball_ofReal, Metric.mem_eball, ENNReal.ofReal_mul (by norm_num), ENNReal.ofReal_ofNat,
         ← Real.rpow_intCast, ← ENNReal.ofReal_rpow_of_pos (realD_pos a),
         ENNReal.ofReal_natCast,ENNReal.rpow_intCast,edist_comm] at hxy'
       have : 0 < (Nat.cast D : ℝ≥0∞) := by

Carleson/ToMathlib/ENorm.lean

@@ -1,4 +1,4 @@
-import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
+import Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
 import Carleson.ToMathlib.Data.ENNReal
 
 -- Upstreaming status: can be upstreamed/being worked on

Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/Basic.lean

@@ -352,7 +352,7 @@ lemma eLorentzNorm'_indicator_const' {a : ε} {s : Set α} (p_ne_zero : p ≠ 0)
       = (p / q) ^ q.toReal⁻¹ * μ s ^ p.toReal⁻¹ * ‖a‖ₑ := by
   rw [eLorentzNorm'_eq p_ne_zero p_ne_top]
   simp_rw [rearrangement_indicator_const]
-  rw [eLpNorm_eq_lintegral_rpow_enorm q_ne_zero q_ne_top]
+  rw [eLpNorm_eq_lintegral_rpow_enorm_toReal q_ne_zero q_ne_top]
   simp only [ENNReal.toReal_inv, enorm_eq_self, one_div]
   conv in (_ * _) ^ _ => rw [ENNReal.mul_rpow_of_nonneg _ _ ENNReal.toReal_nonneg,
     Set.comp_indicator (fun t ↦ t ^ q.toReal),
@@ -520,7 +520,7 @@ lemma MemLorentz_of_MemLorentz_ge {r₁ r₂ : ℝ≥0∞} (r₁_pos : 0 < r₁)
         use ENNReal.rpow_lt_top_of_nonneg (by simp) h₁
         exact (MeasureTheory.memLp_of_memLp_le_of_memLp_ge r₁_pos ⟨r₁_le_r₂, le_top⟩ memLp_r₁ memLp_top).2
       /- Hardest part -/
-      rw [eLpNorm_eq_lintegral_rpow_enorm r₁_pos.ne' r₁_top,
+      rw [eLpNorm_eq_lintegral_rpow_enorm_toReal r₁_pos.ne' r₁_top,
           lintegral_withDensity_eq_lintegral_mul₀ (by measurability) (measurable_mul_distribution_rpow.aestronglyMeasurable.enorm.pow_const r₁.toReal),
           lintegral_nnreal_eq_lintegral_toNNReal_Ioi] at norm_lt_top
       simp only [ENNReal.toReal_inv, enorm_eq_self, Pi.mul_apply, one_div] at norm_lt_top

Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/Defs.lean

@@ -56,7 +56,7 @@ lemma eLorentzNorm'_eq_integral_distribution_rpow {_ : MeasurableSpace α} {f :
   unfold eLorentzNorm'
   simp only [inv_one, ENNReal.toReal_one, ENNReal.rpow_one, ENNReal.toReal_inv]
   congr
-  rw [eLpNorm_eq_lintegral_rpow_enorm (by norm_num) (by norm_num)]
+  rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by norm_num) (by norm_num)]
   rw [lintegral_withDensity_eq_lintegral_mul₀' (by measurability)
     (by apply aeMeasurable_withDensity_inv; apply AEMeasurable.pow_const; apply AEStronglyMeasurable.enorm; apply
       aestronglyMeasurable_iff_aemeasurable.mpr; apply Measurable.aemeasurable; measurability)]

Carleson/ToMathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

@@ -51,7 +51,7 @@ theorem eLpNorm_map_measure' [MeasurableSpace E] [OpensMeasurableSpace E]
   by_cases hp_top : p = ∞
   · rw [hp_top, eLpNorm_exponent_top]
     exact eLpNormEssSup_map_measure' hg hf
-  simp_rw [eLpNorm_eq_lintegral_rpow_enorm hp_zero hp_top]
+  simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp_top]
   rw [lintegral_map' (hg.enorm.pow_const p.toReal) hf]
   rfl
 

Carleson/ToMathlib/RealInterpolation/Minkowski.lean

@@ -739,7 +739,7 @@ lemma estimate_trnc₁ {spf : ScaledPowerFunction} {j : Bool}
       ((sel j p₀ p₁).toReal ⁻¹ * (sel j q₀ q₁).toReal) := by
     congr
     rw [← one_div]
-    refine (eLpNorm_eq_lintegral_rpow_enorm (ε := E₁) ?_ ?_).symm
+    refine (eLpNorm_eq_lintegral_rpow_enorm_toReal (ε := E₁) ?_ ?_).symm
     · exact (interpolated_pos' hp₀ hp₁ (ne_top_of_Ioo ht) hp).ne'
     · exact interp_exp_ne_top hp₀p₁.ne ht hp