chore: bump to v4.24.0 (#502)

Author: Ruben-VandeVelde

Carleson/Antichain/AntichainTileCount.lean

@@ -83,7 +83,7 @@ lemma tile_reach {ϑ : Θ X} {N : ℕ} {p p' : 𝔓 X} (hp : dist_(p) (𝒬 p) 
       ← sub_eq_add_neg, mul_comm _ ((2 : ℝ) ^ _)] at hle
     calc dist_{𝔠 p, 2^((2 : ℤ) - 5*a^2 - 2*a) * D^𝔰 p'} (𝒬 p') o'
       _ ≤ 2^(-(5 : ℤ)*a - 2) * dist_{𝔠 p, 4 * D^𝔰 p'} (𝒬 p') o' := hle
-      _ < 2^(-(5 : ℤ)*a - 2) * 2^(5*a + N + 2) := (mul_lt_mul_left (by positivity)).mpr hlt2
+      _ < 2^(-(5 : ℤ)*a - 2) * 2^(5*a + N + 2) := (mul_lt_mul_iff_right₀ (by positivity)).mpr hlt2
       _ = 2^N := by
         rw [← zpow_natCast, ← zpow_add₀ two_ne_zero]
         simp
@@ -111,7 +111,7 @@ lemma tile_reach {ϑ : Θ X} {N : ℕ} {p p' : 𝔓 X} (hp : dist_(p) (𝒬 p) 
       _ = (4 * 2 ^ (2 - 5 * (a : ℤ)  ^ 2 - 2 * ↑a)) * (D * D ^ 𝔰 p) := by ring
       _ ≤ 4 * 2 ^ (2 - 5 * (a : ℤ)  ^ 2 - 2 * ↑a) * D ^ 𝔰 p' := by
         have h1D : 1 ≤ (D : ℝ) := one_le_realD _
-        nth_rewrite 1 [mul_le_mul_left (by positivity), ← zpow_one (D : ℝ),
+        nth_rewrite 1 [mul_le_mul_iff_right₀ (by positivity), ← zpow_one (D : ℝ),
           ← zpow_add₀ (ne_of_gt (realD_pos _))]
         gcongr
         rw [add_comm]

Carleson/Antichain/Basic.lean

@@ -32,8 +32,9 @@ scoped notation "nnqt" => 2*nnq/(nnq + 1)
 end ShortVariables
 
 lemma inv_nnqt_eq : (nnqt : ℝ)⁻¹ = 2⁻¹ + 2⁻¹ * q⁻¹ := by
-  have : 2 * q ≠ 0 := mul_ne_zero (by norm_num) (by linarith only [(q_mem_Ioc X).1])
-  field_simp [show (nnq : ℝ) = q by rfl]
+  have : q ≠ 0 := by linarith only [(q_mem_Ioc X).1]
+  simp [show (nnq : ℝ) = q by rfl]
+  field_simp
 
 lemma inv_nnqt_mem_Ico : (nnqt : ℝ)⁻¹ ∈ Ico (3 / 4) 1 := by
   rw [inv_nnqt_eq]
@@ -374,14 +375,13 @@ lemma const_check : C6_1_2 a * C2_0_6 (defaultA a) (p X).toNNReal 2 ≤ C6_1_3 a
   have hqiq : q = iq⁻¹ := by rw [iq_eq, inv_inv]
   have : 0 < 1 - iq := by linarith [inv_q_mem_Ico X |>.2]
   have hpdiv' : 2 / (p X) / (2 / (p X).toNNReal - 1).toReal = (2 - iq) * (1 - iq)⁻¹ := by
-    simp only [div_eq_mul_inv, hp_coe', inv_p_eq', ← iq_eq]
-    field_simp [show 2 - iq - 1 = 1 - iq by ring]
+    simp [div_eq_mul_inv, hp_coe', inv_p_eq', ← iq_eq, field, show 2 - iq - 1 = 1 - iq by ring]
   have : 2⁻¹ ≤ iq := inv_q_mem_Ico X |>.1
   have hiq1 : 2 ≤ (1 - iq)⁻¹ := by
     apply (le_inv_comm₀ (by positivity) (by positivity)).mp
     linarith only [inv_q_mem_Ico X |>.1]
   have : 1 < 2 - iq := by linarith only [inv_q_mem_Ico X |>.2]
-  have : 0 < (q - 1)⁻¹ := inv_pos_of_pos <| by linarith only [q_mem_Ioc X |>.1]
+  have : 0 < q - 1 := by linarith only [q_mem_Ioc X |>.1]
   have haux : 1 ≤ (2 - iq) * (1 - iq)⁻¹ * 2 ^ (2 * a) := by
     conv_lhs => rw [← one_mul 1, ← mul_one (1 * 1)]
     gcongr
@@ -405,7 +405,7 @@ lemma const_check : C6_1_2 a * C2_0_6 (defaultA a) (p X).toNNReal 2 ≤ C6_1_3 a
       · rw [mul_comm (2 ^ _)]
         gcongr ?_ * 2 ^ (2 * a)
         calc
-          _ = (2 * q - 1) * (q - 1)⁻¹ := by field_simp [hqiq]
+          _ = (2 * q - 1) * (q - 1)⁻¹ := by simp [hqiq]; field_simp
           _ ≤ _ := by gcongr; linarith only [q_mem_Ioc X |>.2]
   calc
     _ ≤ 2 ^ ((𝕔 + 2) * a ^ 3) * (2 ^ (2 * a + 4) * (q - 1)⁻¹) := by simp [C6_1_2, hc_le]

Carleson/Calculations.lean

@@ -136,7 +136,7 @@ lemma calculation_logD_64 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G
 lemma calculation_5 {dist_1 dist_2 : ℝ}
     (h : dist_1 ≤ (2 ^ (a : ℝ)) ^ (6 : ℝ) * dist_2) :
     2 ^ ((-𝕔 : ℝ) * a) * dist_1 ≤ 2 ^ ((-(𝕔 - 6) : ℝ) * a) * dist_2 := by
-  apply (mul_le_mul_left (show 0 < (2 : ℝ) ^ (𝕔 * (a : ℝ)) by positivity)).mp
+  apply (mul_le_mul_iff_right₀ (show 0 < (2 : ℝ) ^ (𝕔 * (a : ℝ)) by positivity)).mp
   rw [← mul_assoc, neg_mul,
     Real.rpow_neg (by positivity),
     mul_inv_cancel₀ (a := (2 : ℝ) ^ (𝕔 * (a : ℝ))) (by positivity),

Carleson/Classical/Approximation.lean

@@ -63,10 +63,12 @@ lemma fourierCoeffOn_bound {f : ℝ → ℂ} (f_continuous : Continuous f) :
     ∃ C, ∀ n, ‖fourierCoeffOn Real.two_pi_pos f n‖ ≤ C := by
   obtain ⟨C, f_bounded⟩ := continuous_bounded f_continuous.continuousOn
   refine ⟨C, fun n ↦ ?_⟩
-  simp only [fourierCoeffOn_eq_integral, sub_zero, one_div, mul_inv_rev]
+  simp only [fourierCoeffOn_eq_integral, sub_zero, one_div, mul_inv_rev, Complex.real_smul,
+    Complex.norm_real, Complex.norm_mul, norm_eq_abs, abs_mul, abs_inv, Nat.abs_ofNat]
   field_simp
-  rw [abs_of_nonneg pi_pos.le, mul_comm π, div_le_iff₀ Real.two_pi_pos]
-  calc ‖∫ (x : ℝ) in (0 : ℝ)..(2 * π), (starRingEnd ℂ) (Complex.exp (2 * π * Complex.I * n * x / (2 * π))) * f x‖
+  rw [abs_of_nonneg pi_pos.le, mul_comm π]
+  calc
+    _ = ‖∫ (x : ℝ) in (0 : ℝ)..(2 * π), (starRingEnd ℂ) (Complex.exp (2 * π * Complex.I * n * x / (2 * π))) * f x‖ := by simp
     _ = ‖∫ (x : ℝ) in (0 : ℝ)..(2 * π), (starRingEnd ℂ) (Complex.exp (Complex.I * n * x)) * f x‖ := by
       congr with x
       congr
@@ -88,7 +90,7 @@ lemma fourierCoeffOn_bound {f : ℝ → ℂ} (f_continuous : Continuous f) :
       /-Could specify `aestronglyMeasurable` and `intervalIntegrable` intead of `f_continuous`. -/
       exact IntervalIntegrable.intervalIntegrable_norm_iff f_continuous.aestronglyMeasurable |>.mpr
         (f_continuous.intervalIntegrable ..)
-    _ = C * (2 * π) := by simp; ring
+    _ = _ := by simp
 
 /-TODO: Assumptions might be weakened. -/
 lemma periodic_deriv {𝕜 : Type} [NontriviallyNormedField 𝕜] {F : Type} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
@@ -150,9 +152,10 @@ lemma int_sum_nat {β : Type*} [AddCommGroup β] [TopologicalSpace β] [Continuo
   rw [←tendsto_add_atTop_iff_nat 1] at this
   convert this using 1
   ext N
-  induction' N with N ih
-  · simp
-  · have : Icc (- Int.ofNat (N.succ)) (N.succ) = insert (↑(N.succ)) (insert (-Int.ofNat (N.succ)) (Icc (-Int.ofNat N) N)) := by
+  induction N with
+  | zero => simp
+  | succ N ih =>
+    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]
@@ -194,7 +197,7 @@ lemma fourierConv_ofTwiceDifferentiable {f : ℝ → ℂ} (periodicf : f.Periodi
     rw [summable_congr @fourierCoeff_correspondence, ←summable_norm_iff]
     apply summable_of_le_on_nonzero _ _ summable_maj <;> intro i
     · simp
-    · intro ine0; field_simp [maj_def, hC i ine0]
+    · intro ine0; simpa only [maj_def, one_div_mul_eq_div] using hC i ine0
   have := int_sum_nat function_sum
   rw [ContinuousMap.tendsto_iff_tendstoUniformly, Metric.tendstoUniformly_iff] at this
   have := this ε εpos

Carleson/Classical/Basic.lean

@@ -197,7 +197,7 @@ lemma lower_secant_bound_aux {η : ℝ} (ηpos : 0 < η) {x : ℝ} (le_abs_x : 
     _ ≤ (2 / π) * x := by gcongr
     _ = 1 - ((1 - (2 / π) * (x - π / 2)) * Real.cos (π / 2) + ((2 / π) * (x - π / 2)) * Real.cos (π)) := by
       field_simp -- a bit slow
-      ring
+      simp
     _ ≤ 1 - (Real.cos ((1 - (2 / π) * (x - π / 2)) * (π / 2) + (((2 / π) * (x - π / 2)) * (π)))) := by
       gcongr
       apply (strictConvexOn_cos_Icc.convexOn).2 (by simp [pi_nonneg])
@@ -253,7 +253,7 @@ lemma lower_secant_bound' {η : ℝ} {x : ℝ} (le_abs_x : η ≤ |x|) (abs_x_le
         exact mul_le_of_le_div₀ (by norm_num) (div_nonneg (by norm_num) pi_nonneg) (by simpa)
       · exact mul_nonneg (div_nonneg (by norm_num) pi_nonneg) x_nonneg
       · simp
-    _ = Real.sin x := by field_simp
+    _ = Real.sin x := by simp; field_simp
     _ ≤ Real.sqrt ((Real.sin x) ^ 2) := by
       rw [Real.sqrt_sq_eq_abs]
       apply le_abs_self
@@ -282,8 +282,7 @@ lemma lower_secant_bound {η : ℝ} {x : ℝ} (xIcc : x ∈ Set.Icc (-2 * π + 
     rw [mul_assoc]
     gcongr
     field_simp
-    rw [div_le_div_iff₀ (by norm_num) pi_pos]
-    linarith [pi_le_four]
+    norm_num [pi_le_four]
   _ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by
     apply lower_secant_bound' xAbs
     rw [abs_le, neg_sub', sub_neg_eq_add, neg_mul_eq_neg_mul]

Carleson/Classical/DirichletKernel.lean

@@ -209,6 +209,7 @@ lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {x : ℝ}
       congr with n
       rw [fourier_coe_apply, fourier_coe_apply, fourier_coe_apply, ←exp_add]
       congr
+      simp
       field_simp
       ring
 

Carleson/Classical/HilbertKernel.lean

@@ -1,5 +1,5 @@
 import Carleson.Classical.Basic
-import Mathlib.Data.Real.Pi.Bounds
+import Mathlib.Analysis.Real.Pi.Bounds
 
 /- This file contains definitions and lemmas regarding the Hilbert kernel. -/
 

Carleson/Classical/HilbertStrongType.lean

@@ -5,7 +5,7 @@ import Carleson.Defs
 import Carleson.ToMathlib.MeasureTheory.Integral.MeanInequalities
 import Carleson.TwoSidedCarleson.Basic
 import Mathlib.Algebra.BigOperators.Group.Finset.Indicator
-import Mathlib.Data.Real.Pi.Bounds
+import Mathlib.Analysis.Real.Pi.Bounds
 
 /- This file contains the proof that the Hilbert kernel is a bounded operator. -/
 
@@ -223,7 +223,7 @@ lemma spectral_projection_bound {f : ℝ → ℂ} {n : ℕ} (hmf : AEMeasurable
     ← eLpNorm_liftIoc _ _ partialFourierSum_uniformContinuous.continuous.aestronglyMeasurable,
     volume_eq_smul_haarAddCircle,
     eLpNorm_smul_measure_of_ne_top (by trivial), eLpNorm_smul_measure_of_ne_top (by trivial),
-    smul_eq_mul, smul_eq_mul, ENNReal.mul_le_mul_left (by simp [Real.pi_pos]) (by simp)]
+    smul_eq_mul, smul_eq_mul, ENNReal.mul_le_mul_left (by simp [Real.pi_pos]) (by finiteness)]
   have ae_eq_right : F =ᶠ[ae haarAddCircle] liftIoc (2 * π) 0 f := MemLp.coeFn_toLp _
   have ae_eq_left : partialFourierSumLp 2 n F =ᶠ[ae haarAddCircle]
       liftIoc (2 * π) 0 (partialFourierSum n f) :=
@@ -315,7 +315,7 @@ lemma integrable_bump_convolution {f g : ℝ → ℝ}
   have: eLpNorm g 1 (volume.restrict (Ioc 0 (2 * π))) ≠ ⊤ := by
     grw [← lt_top_iff_ne_top,
       eLpNorm_le_eLpNorm_mul_rpow_measure_univ (OrderTop.le_top 1) (hg.restrict _).1]
-    exact ENNReal.mul_lt_top (hg.restrict _).eLpNorm_lt_top (by norm_num)
+    exact ENNReal.mul_lt_top (hg.restrict _).eLpNorm_lt_top (by norm_num; simp [← ENNReal.ofReal_ofNat, ← ENNReal.ofReal_mul])
   rw [← ENNReal.toReal_le_toReal this (by norm_num)]
 
   calc

Carleson/Discrete/ExceptionalSet.lean

@@ -396,7 +396,7 @@ lemma indicator_sum_eq_natCast {s : Finset (𝔓 X)} :
 open scoped Classical in
 lemma layervol_eq_zero_of_lt {t : ℝ} (ht : (𝔐 (X := X) k n).toFinset.card < t) :
     layervol (X := X) k n t = 0 := by
-  rw [layervol, measure_zero_iff_ae_notMem]
+  rw [layervol, measure_eq_zero_iff_ae_notMem]
   refine ae_of_all volume fun x ↦ ?_; rw [mem_setOf, not_le]
   calc
     _ ≤ ((𝔐 (X := X) k n).toFinset.card : ℝ) := by
@@ -658,7 +658,7 @@ lemma tree_count :
   simp_rw [← mul_sum, stackSize_real, mem_coe, filter_univ_mem, interchange, sum_const]
   let _ : PosMulReflectLE ℝ := inferInstance -- perf: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/performance.20example.20with.20type-class.20inference
   -- Replace the cardinality of `𝔘` with the upper bound proven in `card_𝔘m_le`, and simplify.
-  apply le_of_le_of_eq <| (mul_le_mul_left (zpow_pos two_pos _)).mpr <| sum_le_sum <|
+  apply le_of_le_of_eq <| (mul_le_mul_iff_right₀ (zpow_pos two_pos _)).mpr <| sum_le_sum <|
     fun _ _ ↦ smul_le_smul_of_nonneg_right card_𝔘m_le <| Set.indicator_apply_nonneg (by simp)
   simp_rw [← smul_sum, nsmul_eq_mul, ← mul_assoc, filter_mem_univ_eq_toFinset (𝔐 k n), defaultA]
   rw [sub_eq_add_neg, zpow_add₀ two_ne_zero, ← pow_mul, mul_comm 9, mul_comm (2 ^ _)]

Carleson/Discrete/ForestComplement.lean

@@ -1,8 +1,8 @@
 import Carleson.Antichain.AntichainOperator
 import Carleson.Discrete.Defs
 import Carleson.Discrete.SumEstimates
+import Mathlib.Analysis.Complex.ExponentialBounds
 import Mathlib.Combinatorics.Enumerative.DoubleCounting
-import Mathlib.Data.Complex.ExponentialBounds
 
 open MeasureTheory Measure NNReal Metric Complex Set
 open scoped ENNReal
@@ -166,7 +166,7 @@ lemma exists_j_of_mem_𝔓pos_ℭ (h : p ∈ 𝔓pos (X := X)) (mp : p ∈ ℭ k
   rcases B.eq_zero_or_pos with Bz | Bpos
   · simp_rw [B, filter_mem_univ_eq_toFinset, Finset.card_eq_zero, toFinset_eq_empty] at Bz
     exact Or.inl ⟨mp, Bz⟩
-  · right; use Nat.log 2 B; rw [Nat.lt_pow_iff_log_lt one_lt_two Bpos.ne'] at Blt
+  · right; use Nat.log 2 B; rw [← Nat.log_lt_iff_lt_pow one_lt_two Bpos.ne'] at Blt
     refine ⟨by omega, (?_ : _ ∧ _ ≤ B), (?_ : ¬(_ ∧ _ ≤ B))⟩
     · exact ⟨mp, Nat.pow_log_le_self 2 Bpos.ne'⟩
     · rw [not_and, not_le]; exact fun _ ↦ Nat.lt_pow_succ_log_self one_lt_two _
@@ -600,7 +600,7 @@ lemma carlesonSum_𝔓₁_compl_eq_𝔓pos_inter (f : X → ℂ) :
     ∀ᵐ x, x ∈ G \ G' → carlesonSum 𝔓₁ᶜ f x = carlesonSum (𝔓pos (X := X) ∩ 𝔓₁ᶜ) f x := by
   have A p (hp : p ∈ (𝔓pos (X := X))ᶜ) : ∀ᵐ x, x ∈ G \ G' → x ∉ 𝓘 p := by
     simp only [𝔓pos, mem_compl_iff, mem_setOf_eq, not_lt, nonpos_iff_eq_zero] at hp
-    filter_upwards [measure_zero_iff_ae_notMem.mp hp] with x hx h'x (h''x : x ∈ (𝓘 p : Set X))
+    filter_upwards [measure_eq_zero_iff_ae_notMem.mp hp] with x hx h'x (h''x : x ∈ (𝓘 p : Set X))
     simp [h''x, h'x.1, h'x.2] at hx
   rw [← ae_ball_iff (to_countable 𝔓posᶜ)] at A
   filter_upwards [A] with x hx h'x
@@ -997,8 +997,7 @@ lemma lintegral_carlesonSum_𝔓₁_compl_le_sum_aux1 [ProofData a q K σ₁ σ
       + ((q - 1) / (8 * a ^ 4)) ^ 2 * (38 * 1 + 40 * ↑Z)  / (Real.log 2) ^ 2
       + ((q - 1) / (8 * a ^ 4)) * (28 * 1 + 64 * ↑Z) / (Real.log 2) ^ 3
       + (48 * ↑Z) /  (Real.log 2) ^ 4) := by
-    field_simp only
-    ring
+    field_simp
   _ ≤ ((8 * a ^ 4) / (q - 1)) ^ 4 *
      (((2 - 1) / (8 * 4 ^ 4)) ^ 3 * (24 * (Z / 2 ^ 48) + 16 * ↑Z) / 0.69
       + ((2 - 1) / (8 * 4 ^ 4)) ^ 2 * (38 * (Z / 2 ^ 48) + 40 * ↑Z)  / 0.69 ^ 2