chore: bump mathlib and golf (#506)

Fixing two proofs was a bit painful, but otherwise little breakage.
Take advantage of the new mathlib version by golfing a bit using
positivity and the field tactic.

---------

Co-authored-by: Ruben Van de Velde <[email protected]>

Author: grunweg

Carleson.lean

@@ -81,7 +81,6 @@ import Carleson.ToMathlib.MeasureTheory.Measure.NNReal
 import Carleson.ToMathlib.MeasureTheory.Measure.Prod
 import Carleson.ToMathlib.MinLayer
 import Carleson.ToMathlib.Misc
-import Carleson.ToMathlib.Order.Chain
 import Carleson.ToMathlib.Order.LiminfLimsup
 import Carleson.ToMathlib.RealInterpolation.InterpolatedExponents
 import Carleson.ToMathlib.RealInterpolation.LorentzInterpolation

Carleson/Antichain/AntichainOperator.lean

@@ -73,7 +73,7 @@ lemma dens1_antichain_rearrange (bg : BoundedCompactSupport g) :
       exact enorm_integral_mul_starRingEnd_comm
     _ ≤ 2 * ∑ p with p ∈ 𝔄, ∑ p' with p' ∈ 𝔄 ∧ 𝔰 p' ≤ 𝔰 p,
         ‖∫ x, adjointCarleson p g x * conj (adjointCarleson p' g x)‖ₑ := by
-      rw [two_mul]; gcongr with p mp; exact fun _ ↦ And.imp_right Int.le_of_lt
+      rw [two_mul]; gcongr with p mp; exact fun h ↦ h.le
     _ = _ := by congr! 3 with p mp p' mp'; exact enorm_integral_mul_starRingEnd_comm
 
 open Classical in

Carleson/Antichain/AntichainTileCount.lean

@@ -181,7 +181,7 @@ lemma stack_density (𝔄 : Set (𝔓 X)) (ϑ : Θ X) (N : ℕ) (L : Grid X) :
       rw [mem_toFinset] at hp
       calc volume (E p ∩ G)
         _ ≤ volume (E₂ 2 p) := by
-          apply measure_mono (fun x hx ↦ ?_)
+          gcongr; intro x hx
           have hQ : Q x ∈ ball_(p) (𝒬 p) 1 := subset_cball hx.1.2.1
           simp only [E₂, TileLike.toSet, smul_fst, smul_snd, mem_inter_iff, mem_preimage, mem_ball]
           exact ⟨⟨hx.1.1, hx.2⟩, lt_trans hQ one_lt_two⟩
@@ -190,19 +190,24 @@ lemma stack_density (𝔄 : Set (𝔓 X)) (ϑ : Θ X) (N : ℕ) (L : Grid X) :
           have h2a : ((2 : ℝ≥0∞) ^ a)⁻¹ = 2^(-(a : ℤ)) := by
             rw [← zpow_natCast, ENNReal.zpow_neg]
           rw [← ENNReal.div_le_iff (ne_of_gt (hIL ▸ volume_coeGrid_pos (defaultD_pos a)))
-            (by finiteness), ← ENNReal.div_le_iff' (Ne.symm (NeZero.ne' (2 ^ a))) (by finiteness),
+            (by finiteness), ← ENNReal.div_le_iff' (NeZero.ne (2 ^ a)) (by finiteness),
             ENNReal.div_eq_inv_mul, h2a, dens₁]
-          refine le_iSup₂_of_le p hp fun c hc ↦ ?_
-          have h2c : 2 ^ (-(a : ℤ)) * (volume (E₂ 2 p) / volume (L : Set X)) ≤
-              (c : WithTop ℝ≥0) := by
+          refine le_iSup₂_of_le p hp ?_--fun c hc ↦ ?_
+          rw [WithTop.le_iff_forall]
+          intro c hc
+          have h2c : 2 ^ (-(a : ℤ)) * (volume (E₂ 2 p) / volume (L : Set X)) ≤ (c : WithTop ℝ≥0) := by
             simp only [← hc]
-            refine le_iSup₂_of_le 2 (le_refl _) fun d hd ↦ ?_
+            refine le_iSup₂_of_le 2 (le_refl _) ?_
+            rw [WithTop.le_iff_forall]
+            intro d hd
             have h2d : 2 ^ (-(a : ℤ)) * (volume (E₂ 2 p) / volume (L : Set X)) ≤
                 (d : WithTop ℝ≥0)  := by
               rw [← hd]
               gcongr
               · norm_cast
-              · refine le_iSup₂_of_le p (mem_lowerCubes.mpr ⟨p, hp, le_refl _⟩) fun r hr ↦ ?_
+              · refine le_iSup₂_of_le p (mem_lowerCubes.mpr ⟨p, hp, le_refl _⟩) ?_
+                rw [WithTop.le_iff_forall]
+                intro r hr
                 have h2r : (volume (E₂ 2 p) / volume (L : Set X)) ≤ (r : WithTop ℝ≥0)  := by
                   rw [← hr]
                   refine le_iSup_of_le (le_refl _) ?_

Carleson/Antichain/Basic.lean

@@ -182,10 +182,7 @@ lemma maximal_bound_antichain {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤
         rw [carlesonSum, Finset.sum_eq_single_of_mem p.1 hp hne_p]
     _ ≤ ∫⁻ y, ‖exp (I * (Q x y - Q x x)) * Ks (𝔰 p.1) x y * f y‖ₑ := by
         rw [carlesonOn, indicator, if_pos hxE]
-        refine le_trans (enorm_integral_le_lintegral_enorm _) (lintegral_mono fun z w h ↦ ?_)
-        simp only [nnnorm_mul, coe_mul, some_eq_coe', zpow_neg, Ks, mul_assoc,
-          enorm_eq_nnnorm] at h ⊢
-        use w
+        exact le_trans (enorm_integral_le_lintegral_enorm _) (lintegral_mono fun z ↦ le_rfl)
     _ ≤ ∫⁻ y, ‖Ks (𝔰 p.1) x y * f y‖ₑ := by
       simp only [enorm_mul]
       exact lintegral_mono fun y ↦ (by simp [← Complex.ofReal_sub])

Carleson/Antichain/TileCorrelation.lean

@@ -350,10 +350,10 @@ lemma I12_le' {p p' : 𝔓 X} (hle : 𝔰 p' ≤ 𝔰 p) {g : X → ℂ} (x1 : E
         C2_0_5 a * volume (ball x1.1 (D ^ 𝔰 p')) *
         (C6_2_1 a / (volume (ball x1.1 (D ^ 𝔰 p')) * volume (ball x2.1 (D ^ 𝔰 p)))) := by
       gcongr
-    -- Note: simp, ring_nf, field_simp did not help.
+    -- Note: simp, ring_nf, field_simp did not help (because we work with ℝ≥0∞).
     have heq : C2_0_5 a * volume (ball x1.1 (D ^ 𝔰 p')) *
-      (C6_2_1 a / (volume (ball x1.1 (D ^ 𝔰 p')) * volume (ball x2.1 (D ^ 𝔰 p)))) =
-      C2_0_5 a * (C6_2_1 a / volume (ball x2.1 (D ^ 𝔰 p))) := by
+        (C6_2_1 a / (volume (ball x1.1 (D ^ 𝔰 p')) * volume (ball x2.1 (D ^ 𝔰 p)))) =
+        C2_0_5 a * (C6_2_1 a / volume (ball x2.1 (D ^ 𝔰 p))) := by
       simp only [mul_assoc]
       congr 1
       rw [ENNReal.div_eq_inv_mul, ENNReal.mul_inv (.inr measure_ball_ne_top)

Carleson/Classical/Basic.lean

@@ -4,6 +4,7 @@ import Carleson.ToMathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
 import Carleson.ToMathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
 import Carleson.ToMathlib.Topology.Instances.AddCircle.Defs
 import Mathlib.Analysis.Fourier.AddCircle
+import Mathlib.Tactic.Field
 
 /- This file contains basic definitions and lemmas. -/
 
@@ -196,7 +197,7 @@ lemma lower_secant_bound_aux {η : ℝ} (ηpos : 0 < η) {x : ℝ} (le_abs_x : 
   calc (2 / π) * η
     _ ≤ (2 / π) * x := by gcongr
     _ = 1 - ((1 - (2 / π) * (x - π / 2)) * Real.cos (π / 2) + ((2 / π) * (x - π / 2)) * Real.cos (π)) := by
-      field_simp -- a bit slow
+      field_simp
       simp
     _ ≤ 1 - (Real.cos ((1 - (2 / π) * (x - π / 2)) * (π / 2) + (((2 / π) * (x - π / 2)) * (π)))) := by
       gcongr
@@ -207,7 +208,7 @@ lemma lower_secant_bound_aux {η : ℝ} (ηpos : 0 < η) {x : ℝ} (le_abs_x : 
         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) (by linarith [h])
       · simp
-    _ = 1 - Real.cos x := by congr; field_simp; ring -- slow
+    _ = 1 - Real.cos x := by congr; field
     _ ≤ Real.sqrt ((1 - Real.cos x) ^ 2) := by
       exact Real.sqrt_sq_eq_abs _ ▸ le_abs_self _
     _ ≤ ‖1 - Complex.exp (Complex.I * ↑x)‖ := by

Carleson/Classical/ControlApproximationEffect.lean

@@ -497,7 +497,8 @@ lemma C_control_approximation_effect_pos {ε : ℝ} (εpos : 0 < ε) : 0 < C_con
   lt_trans' (lt_C_control_approximation_effect εpos) pi_pos
 
 lemma C_control_approximation_effect_eq {ε : ℝ} {δ : ℝ} (ε_nonneg : 0 ≤ ε) :
-    C_control_approximation_effect ε * δ = ((δ * C10_0_1 4 2 * (4 * π) ^ (2 : ℝ)⁻¹ * (2 / ε) ^ (2 : ℝ)⁻¹) / π) + π * δ := by
+    C_control_approximation_effect ε * δ =
+      ((δ * C10_0_1 4 2 * (4 * π) ^ (2 : ℝ)⁻¹ * (2 / ε) ^ (2 : ℝ)⁻¹) / π) + π * δ := by
   symm
   rw [C_control_approximation_effect, mul_comm, mul_div_right_comm, mul_comm δ, mul_assoc,
     mul_comm δ, ← mul_assoc, ← mul_assoc, ← add_mul, mul_comm _ (C10_0_1 4 2 : ℝ), mul_assoc]
@@ -507,13 +508,28 @@ lemma C_control_approximation_effect_eq {ε : ℝ} {δ : ℝ} (ε_nonneg : 0 ≤
     ring_nf
     try rw [mul_assoc, mul_comm (2 ^ _), mul_assoc, mul_assoc, mul_assoc, mul_comm (4 ^ _), ← mul_assoc π⁻¹,
       ← Real.rpow_neg_one π, ← Real.rpow_add, mul_comm (π ^ _), ← mul_assoc (2 ^ _), ← Real.mul_rpow]
-  on_goal 1 => congr
-  · norm_num
-  on_goal 1 => ring_nf
-  on_goal 1 => rw [neg_div, Real.rpow_neg]
+  on_goal 1 =>
+    field_simp
+    ring_nf
+    calc _
+      _ = (π ^ (1 / (2 : ℝ))) ^ 2 * 2 ^ (1 / (2 : ℝ)) * (ε ^ (1 / (2 : ℝ)))⁻¹ * 2 := by ring
+      _ = π * 2 ^ (1 / (2 : ℝ)) * (ε ^ (1 / (2 : ℝ)))⁻¹ * 2 := by
+        -- Golfing of this proof welcome!
+        congr
+        rw [← Real.sqrt_eq_rpow π, Real.sq_sqrt', max_eq_left_iff]
+        positivity
+      _ = π * (2 ^ (1 / (2 : ℝ)) * 2) * (ε ^ (1 / (2 : ℝ)))⁻¹ := by ring
+      _ = π * 8 ^ (1 / (2 : ℝ)) * (ε ^ (1 / (2 : ℝ)))⁻¹  := by
+        congr
+        -- Golfing of this computation is very welcome!
+        rw [← Real.sqrt_eq_rpow, ← Real.sqrt_eq_rpow]
+        have : Real.sqrt 4 = 2 := Real.sqrt_eq_cases.mpr <| Or.inl ⟨by norm_num, by positivity⟩
+        nth_rw 2 [← this]
+        rw [← Real.sqrt_mul (by positivity) 4]
+        norm_num
+      _ = (ε ^ (1 / (2 : ℝ)))⁻¹ * π * 8 ^ (1 / (2 : ℝ)) := by ring
   all_goals linarith [pi_pos]
 
-
 /- This is Lemma 11.6.4 (partial Fourier sums of small) in the blueprint.-/
 lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ : 0 < δ)
     {h : ℝ → ℂ} (h_measurable : Measurable h)

Carleson/Classical/DirichletKernel.lean

@@ -2,6 +2,7 @@
 
 import Carleson.Classical.Basic
 import Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
+import Mathlib.Tactic.Field
 
 open scoped Real
 open Finset Complex MeasureTheory
@@ -165,6 +166,7 @@ lemma norm_dirichletKernel'_le {x : ℝ} : ‖dirichletKernel' N x‖ ≤ 2 * N
     rw [dirichletKernel'_eq_zero h, norm_zero]
     linarith
 
+set_option linter.flexible false in -- linter bug; fix pending in mathlib
 /-- First part of lemma 11.1.8 (Dirichlet kernel) from the blueprint. -/
 lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {x : ℝ}
     (h : IntervalIntegrable f volume 0 (2 * π)) :
@@ -198,8 +200,7 @@ lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {x : ℝ}
       rw [fourier_coe_apply, fourier_coe_apply, fourier_coe_apply, ←exp_add]
       congr
       simp
-      field_simp
-      ring
+      field
 
 lemma partialFourierSum_eq_conv_dirichletKernel' {f : ℝ → ℂ} {x : ℝ}
     (h : IntervalIntegrable f volume 0 (2 * π)) :

Carleson/Classical/HilbertStrongType.lean

@@ -6,6 +6,7 @@ import Carleson.ToMathlib.MeasureTheory.Integral.MeanInequalities
 import Carleson.TwoSidedCarleson.Basic
 import Mathlib.Algebra.BigOperators.Group.Finset.Indicator
 import Mathlib.Analysis.Real.Pi.Bounds
+import Mathlib.Tactic.Field
 
 /- This file contains the proof that the Hilbert kernel is a bounded operator. -/
 
@@ -160,9 +161,7 @@ lemma niceKernel_lowerBound {r x : ℝ} (hr : 0 < r) (h'r : r < 1) (hx : r ≤ x
     gcongr
     · apply le_inv_of_le_inv₀ hr (by simpa using h'r.le)
     · exact hx.1
-  _ = 5 * r ⁻¹ := by
-    field_simp
-    ring
+  _ = 5 * r ⁻¹ := by field_simp; norm_num
 
 lemma niceKernel_lowerBound' {r x : ℝ} (hr : 0 < r) (h'r : r < 1) (hx : r ≤ |x| ∧ |x| ≤ π) :
     1 + r / ‖1 - exp (I * x)‖ ^ 2 ≤ 5 * niceKernel r x := by

Carleson/Discrete/ForestComplement.lean

@@ -153,9 +153,11 @@ lemma exists_j_of_mem_𝔓pos_ℭ (h : p ∈ 𝔓pos (X := X)) (mp : p ∈ ℭ k
   let B : ℕ := Finset.card { q | q ∈ 𝔅 k n p }
   have Blt : B < 2 ^ (2 * n + 4) := by
     calc
-      _ ≤ Finset.card { m | m ∈ 𝔐 k n ∧ x ∈ 𝓘 m } :=
-        Finset.card_le_card (Finset.monotone_filter_right _ (Pi.le_def.mpr fun m ⟨m₁, m₂⟩ ↦
-          ⟨m₁, m₂.1.1 mx⟩))
+      _ ≤ Finset.card { m | m ∈ 𝔐 k n ∧ x ∈ 𝓘 m } := by
+        apply Finset.card_le_card (Finset.monotone_filter_right _ ?_)
+        refine fun a _ha ha' ↦ ⟨mem_of_mem_inter_left ha', ?_⟩
+        obtain ⟨m₁, m₂⟩ := ha'
+        exact m₂.1.1 mx
       _ = stackSize (𝔐 k n) x := by
         simp_rw [stackSize, indicator_apply, Pi.one_apply, Finset.sum_boole, Nat.cast_id,
           Finset.filter_filter]; rfl
@@ -917,7 +919,7 @@ lemma lintegral_enorm_carlesonSum_le_of_isAntichain_subset_ℭ
          · norm_cast
            linarith [four_le_a X]
          · exact q_le_two X
-      _ = 5 / (8 * a ^ 3) := by field_simp; ring
+      _ = 5 / (8 * a ^ 3) := by field_simp; norm_num
       _ ≤ 5 / (8 * (4 : ℝ) ^ 3) := by gcongr
       _ ≤ 2⁻¹ := by norm_num
     · calc