chore: bump to v4.26.0 (#522)

Author: Ruben-VandeVelde

Carleson/Antichain/AntichainOperator.lean

@@ -264,7 +264,7 @@ lemma dens1_antichain_sq (h𝔄 : IsAntichain (· ≤ ·) 𝔄)
     _ ≤ Tile.C6_1_5 a * 2 ^ (6 * a + 1) * ∑ p with p ∈ 𝔄,
         ∫⁻ y in E p, C6_1_6 a * dens₁ 𝔄 ^ (p₆ a)⁻¹ * M14 𝔄 (q₆ a) g y * ‖g y‖ₑ := by
       gcongr with p mp; rw [← lintegral_const_mul _ hg.enorm]
-      refine setLIntegral_mono' measurableSet_E fun x mx ↦ mul_le_mul_right' ?_ _
+      refine setLIntegral_mono' measurableSet_E fun x mx ↦ mul_le_mul_left ?_ _
       rw [Finset.mem_filter_univ] at mp
       refine dach_bound h𝔄 mp hg hgG <|
         ((E_subset_𝓘.trans Grid_subset_ball).trans (ball_subset_ball ?_)) mx

Carleson/Antichain/AntichainTileCount.lean

@@ -286,7 +286,7 @@ lemma stack_density (𝔄 : Set (𝔓 X)) (ϑ : Θ X) (N : ℕ) (L : Grid X) :
         gcongr
         norm_cast
         calc 𝔄'.toFinset.card * 2 ^ a
-          _ ≤ 2 ^ (a * (N + 4)) * 2 ^ a := mul_le_mul_right' hcard _
+          _ ≤ 2 ^ (a * (N + 4)) * 2 ^ a := mul_le_mul_left hcard _
           _ = 2 ^ (a * (N + 5)) := by ring
       _ ≤ 2 ^ (a * (N + 5)) * dens₁  (𝔄 : Set (𝔓 X)) * volume (L : Set X) := by
         have hss : 𝔄' ⊆ 𝔄 := by

Carleson/Antichain/Basic.lean

@@ -217,7 +217,7 @@ lemma maximal_bound_antichain {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤
       · exact lt_of_le_of_lt hdist_cp
           (mul_lt_mul_of_nonneg_of_pos (by linarith) (le_refl _) (by linarith) hDpow_pos)
     _ ≤ C6_1_2 a * MB volume 𝔄 𝔠 (8 * D ^ 𝔰 ·) f x := by
-      rw [mul_le_mul_left (C6_1_2_ne_zero a) coe_ne_top, MB, maximalFunction,
+      rw [ENNReal.mul_le_mul_iff_right (C6_1_2_ne_zero a) coe_ne_top, MB, maximalFunction,
         inv_one, ENNReal.rpow_one, le_iSup_iff]
       simp only [iSup_le_iff, ENNReal.rpow_one]
       exact (fun _ hc ↦ hc p.1 p.2)

Carleson/Antichain/TileCorrelation.lean

@@ -269,7 +269,7 @@ lemma uncertainty' (ha : 1 ≤ a) {p₁ p₂ : 𝔓 X} (hle : 𝔰 p₁ ≤ 𝔰
       have hpow : (2 : ℝ) + 2 ^ (6 * a) ≤ 2 ^ (a * 8) :=
         calc
           _ ≤ (2 : ℝ) ^ (6 * a) + 2 ^ (6 * a) := by
-            apply add_le_add_right
+            apply add_le_add_left
             norm_cast
             nth_rw 1 [← pow_one 2]
             exact Nat.pow_le_pow_right zero_lt_two (by cutsat)
@@ -430,7 +430,7 @@ lemma bound_6_2_29 (ha : 4 ≤ a) {p p' : 𝔓 X} (x2 : E p) :
     C6_1_5 a *
     (1 + edist_(p') (𝒬 p') (𝒬 p)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) / volume (𝓘 p : Set X) := by
   rw [mul_comm, mul_div_assoc, mul_comm (C6_1_5 a : ℝ≥0∞), mul_div_assoc]
-  refine mul_le_mul_left' ?_ _
+  refine mul_le_mul_right ?_ _
   calc
     _ = 2 ^ ((2 * 𝕔 + 6 + 𝕔 / 4) * a ^ 3 + 1) * 2 ^ (11 * a) * 2 ^ (-(3 : ℤ) * a) /
         volume (ball x2.1 (D ^ 𝔰 p)) := by

Carleson/Classical/Approximation.lean

@@ -158,7 +158,7 @@ lemma int_sum_nat {β : Type*} [AddCommGroup β] [TopologicalSpace β] [Continuo
     have : Icc (- Int.ofNat (N.succ)) (N.succ) = insert (↑(N.succ)) (insert (-Int.ofNat (N.succ)) (Icc (-Int.ofNat N) N)) := by
       rw [←Ico_insert_right, ←Ioo_insert_left]
       · congr 2 with n
-        simp only [Int.ofNat_eq_coe, mem_Ioo, mem_Icc]
+        simp only [Int.ofNat_eq_natCast, mem_Ioo, mem_Icc]
         push_cast
         rw [Int.lt_add_one_iff, neg_add, ←sub_eq_add_neg, Int.sub_one_lt_iff]
       · norm_num
@@ -169,7 +169,7 @@ lemma int_sum_nat {β : Type*} [AddCommGroup β] [TopologicalSpace β] [Continuo
     · symm
       rw [sum_range_succ, add_comm, ←add_assoc, add_comm]
       simp only [Nat.cast_add, Nat.cast_one, neg_add_rev, Int.reduceNeg, Nat.succ_eq_add_one,
-        Int.ofNat_eq_coe, add_comm]
+        Int.ofNat_eq_natCast, add_comm]
     · simp
     · norm_num
       linarith

Carleson/Classical/Basic.lean

@@ -20,7 +20,6 @@ theorem fourierCoeff_eq_fourierCoeff_of_aeeq {T : ℝ} [hT : Fact (0 < T)] {n :
   apply integral_congr_ae
   change @DFunLike.coe C(AddCircle T, ℂ) (AddCircle T) (fun x ↦ ℂ) ContinuousMap.instFunLike (fourier (-n)) * f =ᶠ[ae haarAddCircle] @DFunLike.coe C(AddCircle T, ℂ) (AddCircle T) (fun x ↦ ℂ) ContinuousMap.instFunLike (fourier (-n)) * g
   have fourier_measurable : AEStronglyMeasurable (⇑(@fourier T (-n))) haarAddCircle := (ContinuousMap.measurable _).aestronglyMeasurable
-
   rw [← AEEqFun.mk_eq_mk (hf := fourier_measurable.mul hf) (hg := fourier_measurable.mul hg),
       ← AEEqFun.mk_mul_mk _ _ fourier_measurable hf, ← AEEqFun.mk_mul_mk _ _ fourier_measurable hg]
   congr 1
@@ -37,7 +36,7 @@ lemma partialFourierSum_eq_partialFourierSum' [hT : Fact (0 < 2 * Real.pi)] (N :
   ext x
   unfold partialFourierSum partialFourierSum' liftIoc
   simp only [
-    Function.comp_apply, Set.restrict_apply, Int.ofNat_eq_coe, ContinuousMap.coe_sum,
+    Function.comp_apply, Set.restrict_apply, Int.ofNat_eq_natCast, ContinuousMap.coe_sum,
     ContinuousMap.coe_smul, Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
   congr
   ext n

Carleson/Classical/CarlesonOnTheRealLine.lean

@@ -250,7 +250,6 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R} :
   set m₁ := Int.floor (f - R' / (2 * R)) with m₁def
   set! m₂ := f with m₂def
   set m₃ := Int.ceil (f + R' / (2 * R)) with m₃def
-
   /- classical is necessary to be able to build a Finset of WithFunctionDistance. -/
   classical
   set balls : Finset (WithFunctionDistance x R) := {m₁, m₂, m₃} with balls_def

Carleson/Classical/ClassicalCarleson.lean

@@ -19,7 +19,6 @@ theorem exceptional_set_carleson {f : ℝ → ℂ}
   set ε' := ε / 4 / C_control_approximation_effect ε with ε'def
   have ε'pos : ε' > 0 := div_pos (div_pos εpos (by norm_num))
     (C_control_approximation_effect_pos εpos)
-
   /- Approximate f by a smooth f₀. -/
   have unicont_f : UniformContinuous f := periodic_f.uniformContinuous_of_continuous
     Real.two_pi_pos cont_f.continuousOn
@@ -33,19 +32,17 @@ theorem exceptional_set_carleson {f : ℝ → ℂ}
   have h_bound : ∀ x, ‖h x‖ ≤ ε' := by
     intro x
     simpa only [hdef, Pi.sub_apply, norm_sub_rev] using hf₀ x
-
   /- Control approximation effect: Get a bound on the partial Fourier sums of h. -/
   obtain ⟨E, Esubset, Emeasurable, Evolume, hE⟩ := control_approximation_effect εpos ε'pos
     h_measurable h_periodic h_bound
-
   /- This is a classical "epsilon third" argument. -/
   use E, Esubset, Emeasurable, Evolume, N₀
   intro x hx N NgtN₀
   calc ‖f x - S_ N f x‖
   _ = ‖(f x - f₀ x) + (f₀ x - S_ N f₀ x) + (S_ N f₀ x - S_ N f x)‖ := by ring_nf
   _ ≤ ‖(f x - f₀ x) + (f₀ x - S_ N f₀ x)‖ + ‖S_ N f₀ x - S_ N f x‖ := norm_add_le ..
   _ ≤ ‖f x - f₀ x‖ + ‖f₀ x - S_ N f₀ x‖ + ‖S_ N f₀ x - S_ N f x‖ :=
-    add_le_add_right (norm_add_le ..) _
+    add_le_add_left (norm_add_le ..) _
   _ ≤ ε' + (ε / 4) + (ε / 4) := by
     gcongr
     · exact hf₀ x
@@ -66,17 +63,14 @@ theorem exceptional_set_carleson {f : ℝ → ℂ}
 theorem carleson_interval {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (2 * π)) :
     ∀ᵐ x ∂volume.restrict (Set.Icc 0 (2 * π)),
       Filter.Tendsto (S_ · f x) Filter.atTop (nhds (f x)) := by
-
   let δ (k : ℕ) : ℝ := 1 / (k + 1) --arbitrary sequence tending to zero
   have δconv : Filter.Tendsto δ Filter.atTop (nhds 0) := tendsto_one_div_add_atTop_nhds_zero_nat
   have δpos (k : ℕ) : 0 < δ k := by apply div_pos zero_lt_one (by linarith)
-
   -- ENNReal version to be comparable to volumes
   let δ' (k : ℕ) := ENNReal.ofReal (δ k)
   have δ'conv : Filter.Tendsto δ' Filter.atTop (nhds 0) := by
     rw [← ENNReal.ofReal_zero]
     exact ENNReal.tendsto_ofReal δconv
-
   set ε := fun k n ↦ (1 / 2) ^ n * 2⁻¹ * δ k with εdef
   have εpos (k n : ℕ) : 0 < ε k n := by positivity
   have εsmall (k : ℕ) {e : ℝ} (epos : 0 < e) : ∃ n, ε k n < e := by
@@ -91,7 +85,6 @@ theorem carleson_interval {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f
     use n
     convert (hn n (by simp))
     simp_rw [dist_zero_right, Real.norm_eq_abs, abs_of_nonneg (εpos k n).le]
-
   have δ'_eq {k : ℕ} : δ' k = ∑' n, ENNReal.ofReal (ε k n) := by
     rw [εdef]
     conv => rhs; pattern ENNReal.ofReal _; rw [ENNReal.ofReal_mul' (δpos k).le,
@@ -102,43 +95,35 @@ theorem carleson_interval {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f
     conv => pattern ENNReal.ofReal _; ring_nf; rw [ENNReal.ofReal_one]
     · rw [one_mul]
     norm_num
-
   -- Main step: Apply exceptional_set_carleson to get a family of exceptional sets parameterized by ε.
   choose Eε hEε_subset _ hEε_measure hEε using (@exceptional_set_carleson f cont_f periodic_f)
-
   have Eεmeasure {ε : ℝ} (hε : 0 < ε) : volume (Eε hε) ≤ ENNReal.ofReal ε := by
     rw [ENNReal.le_ofReal_iff_toReal_le _ hε.le]
     · exact hEε_measure hε
     · rw [← lt_top_iff_ne_top]
       apply lt_of_le_of_lt (measure_mono (hEε_subset hε)) measure_Icc_lt_top
-
   -- Define exceptional sets parameterized by δ.
   let Eδ (k : ℕ) := ⋃ (n : ℕ), Eε (εpos k n)
   have Eδmeasure (k : ℕ) : volume (Eδ k) ≤ δ' k := by
     apply le_trans (measure_iUnion_le _)
     rw [δ'_eq]
     exact ENNReal.tsum_le_tsum (fun n ↦ Eεmeasure (εpos k n))
-
   -- Define final exceptional set.
   let E := ⋂ (k : ℕ), Eδ k
-
   -- Show that it has the desired property.
   have hE : ∀ x ∈ (Set.Icc 0 (2 * π)) \ E, Filter.Tendsto (S_ · f x) Filter.atTop (nhds (f x)) := by
     intro x hx
     rw [Set.diff_iInter, Set.mem_iUnion] at hx
     rcases hx with ⟨k,hk⟩
     rw [Set.diff_iUnion, Set.mem_iInter] at hk
-
     rw [Metric.tendsto_atTop']
     intro e epos
     rcases (εsmall k epos) with ⟨n, lt_e⟩
-
     rcases (hEε (εpos k n)) with ⟨N₀,hN₀⟩
     use N₀
     intro N hN
     rw [dist_comm, dist_eq_norm]
     exact (hN₀ x (hk n) N hN).trans_lt lt_e
-
   -- Show that is has measure zero.
   have Emeasure : volume E ≤ 0 := by
     have : ∀ k, volume E ≤ δ' k := by
@@ -147,7 +132,6 @@ theorem carleson_interval {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f
       apply measure_mono
       apply Set.iInter_subset
     exact ge_of_tendsto' δ'conv this
-
   -- Use results to prove the statement.
   rw [ae_restrict_iff' measurableSet_Icc]
   apply le_antisymm _ (zero_le _)

Carleson/Classical/ControlApproximationEffect.lean

@@ -288,7 +288,7 @@ lemma le_CarlesonOperatorReal {g : ℝ → ℂ} (hg : IntervalIntegrable g volum
       congr
       rw [Dirichlet_Hilbert_eq]
       simp only [ofReal_sub, mul_comm, mul_neg, ← mul_assoc, k, map_mul, ← exp_conj, map_neg,
-        conj_I, map_sub, conj_ofReal, map_natCast, neg_neg, map_div₀, map_one, Int.ofNat_eq_coe,
+        conj_I, map_sub, conj_ofReal, map_natCast, neg_neg, map_div₀, map_one, Int.ofNat_eq_natCast,
         Int.cast_natCast, K, ← exp_add, map_add]
       ring_nf
     _ ≤ ⨆ (n : ℤ) (r : ℝ) (_ : 0 < r) (_ : r < 1), ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, g y * (exp (I * (-n * x)) * K x y * exp (I * n * y) + conj (exp (I * (-n * x)) * K x y * exp (I * n * y)))‖ₑ := by
@@ -330,12 +330,12 @@ lemma le_CarlesonOperatorReal {g : ℝ → ℂ} (hg : IntervalIntegrable g volum
           have integrable₁ := integrable_annulus hx hg rpos.le rle1
           rw [integral_add]
           · conv => pattern ((g _) * _); rw [mul_comm]
-            apply Integrable.bdd_mul' integrable₁ measurable₁.aestronglyMeasurable
+            apply Integrable.bdd_mul integrable₁ measurable₁.aestronglyMeasurable
             · rw [ae_restrict_iff' annulus_measurableSet]
               on_goal 1 => apply Eventually.of_forall
               exact fun _ hy ↦ boundedness₁ hy.1.le
           · conv => pattern ((g _) * _); rw [mul_comm]
-            apply Integrable.bdd_mul' integrable₁ (by fun_prop)
+            apply Integrable.bdd_mul integrable₁ (by fun_prop)
             · rw [ae_restrict_iff' annulus_measurableSet]
               · apply Eventually.of_forall
                 intro y hy
@@ -397,7 +397,6 @@ lemma partialFourierSum_bound {δ : ℝ} (hδ : 0 < δ) {g : ℝ → ℂ} (measu
         rw [← intervalIntegral.integral_add (intervalIntegrable_mul_dirichletKernel'_max hx intervalIntegrable_g) (intervalIntegrable_mul_dirichletKernel'_max' hx intervalIntegrable_g)]
         congr with y
         ring
-
   calc
     _ ≤ (‖∫ y in (x - π)..(x + π), g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖ₑ
         + ‖∫ y in (x - π)..(x + π), g y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖ₑ) / ENNReal.ofReal (2 * π) := by
@@ -413,7 +412,6 @@ lemma partialFourierSum_bound {δ : ℝ} (hδ : 0 < δ) {g : ℝ → ℂ} (measu
         norm_cast
         apply NNReal.le_toNNReal_of_coe_le
         rw [coe_nnnorm]
-
         calc ‖∫ (y : ℝ) in x - π..x + π, g y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖
           _ ≤ (δ * π) * |(x + π) - (x - π)| := by
             apply intervalIntegral.norm_integral_le_of_norm_le_const
@@ -560,7 +558,6 @@ lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ :
     intro x
     simp only [RCLike.star_def, Function.comp_apply, RingHomIsometric.norm_map]
     exact h_bound x
-
   have le_operator_add : ∀ x ∈ E, ENNReal.ofReal ((ε' - π * δ) * (2 * π)) ≤ T h x + T (conj ∘ h) x := by
     intro x hx
     obtain ⟨xIcc, N, hN⟩ := hx

Carleson/Classical/DirichletKernel.lean

@@ -26,7 +26,7 @@ lemma continuous_dirichletKernel : Continuous (dirichletKernel N) := by
 
 lemma dirichletKernel_periodic : Function.Periodic (dirichletKernel N) (2 * π) := by
   intro x
-  simp only [dirichletKernel, Int.ofNat_eq_coe, AddSubgroup.mem_zmultiples,
+  simp only [dirichletKernel, Int.ofNat_eq_natCast, AddSubgroup.mem_zmultiples,
     QuotientAddGroup.mk_add_of_mem, fourier_apply, fourier_coe_apply', ofReal_mul, ofReal_ofNat]
 
 lemma dirichletKernel'_periodic : Function.Periodic (dirichletKernel' N) (2 * π) := by