chore: bump mathlib (#527)

* Original motivation: can
leanprover-community/mathlib4#34023 be used to
golf some proofs?
* When leanprover-community/mathlib4#34039
(`finiteness [h, h']` syntax) is merged, it will also be interesting to
try using it more.
* And leanprover-community/mathlib4#34133
(positivity bugfix) might also help with using positivity/finiteness
more.

---------

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Author: grunweg

Carleson/Discrete/ExceptionalSet.lean

@@ -669,7 +669,7 @@ lemma tree_count :
 lemma boundary_exception {u : 𝔓 X} :
     volume (⋃ i ∈ 𝓛 (X := X) n u, (i : Set X)) ≤ C5_2_9 X n * volume (𝓘 u : Set X) := by
   by_cases  h_𝓛_n_u_non_empty : Set.Nonempty (𝓛 (X := X) n u)
-  · set X_u := { x ∈ GridStructure.coeGrid (𝓘 u) | EMetric.infEdist x (GridStructure.coeGrid (𝓘 u))ᶜ ≤ 12 * (D ^ (𝔰 u - Z * (n + 1) - 1 : ℤ) : ℝ≥0∞)} with h_X_u -- 5.2.25
+  · set X_u := { x ∈ GridStructure.coeGrid (𝓘 u) | Metric.infEDist x (GridStructure.coeGrid (𝓘 u))ᶜ ≤ 12 * (D ^ (𝔰 u - Z * (n + 1) - 1 : ℤ) : ℝ≥0∞)} with h_X_u -- 5.2.25
     calc volume (⋃ i ∈ 𝓛 (X := X) n u, (i : Set X))
       _ ≤ volume X_u := by
           have i_subset_X_u : ∀ i ∈ 𝓛 (X := X) n u, GridStructure.coeGrid i ⊆ X_u := by
@@ -693,8 +693,8 @@ lemma boundary_exception {u : 𝔓 X} :
                     rel [dist_bpt_c_i_le]
                 _ ≤ 12 * D ^ s i := by linarith
             -- show the the triangle inequality implies distance between ipt and (𝓘 u)ᶜ <= 12 * D ^ s i
-            calc EMetric.infEdist ipt (GridStructure.coeGrid (𝓘 u))ᶜ
-              _ ≤ edist ipt bpt := EMetric.infEdist_le_edist_of_mem <| Set.mem_compl h_bpt_not_in_I_u
+            calc Metric.infEDist ipt (GridStructure.coeGrid (𝓘 u))ᶜ
+              _ ≤ edist ipt bpt := Metric.infEDist_le_edist_of_mem <| Set.mem_compl h_bpt_not_in_I_u
               _ ≤ ENNReal.ofReal (12 * D ^ s i) := by
                 rw [edist_dist]
                 exact ENNReal.ofReal_le_ofReal ipt_bpt_triangle_ineq
@@ -740,7 +740,7 @@ lemma boundary_exception {u : 𝔓 X} :
                    show 𝔰 u = s (𝓘 u) from rfl, add_comm,
                    neg_add_eq_sub] at small_boundary_h_intermediate
             have small_b := GridStructure.small_boundary small_boundary_h
-            have X_u_in_terms_of_t : X_u = { x ∈ GridStructure.coeGrid (𝓘 u) | EMetric.infEdist x (GridStructure.coeGrid (𝓘 u))ᶜ ≤ ((t * D ^ (s (𝓘 u))):ℝ≥0∞)} := by
+            have X_u_in_terms_of_t : X_u = { x ∈ GridStructure.coeGrid (𝓘 u) | Metric.infEDist x (GridStructure.coeGrid (𝓘 u))ᶜ ≤ ((t * D ^ (s (𝓘 u))):ℝ≥0∞)} := by
               rw [ht, show s (𝓘 u) = 𝔰 u from rfl,
                   show (D ^ 𝔰 u : ℝ≥0∞) = (D ^ 𝔰 u : ℝ≥0) by simp]
               rw_mod_cast [D_pow_algebra, h_X_u]

Carleson/ForestOperator/LargeSeparation.lean

@@ -1404,7 +1404,7 @@ lemma global_tree_control1_supbound (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (h
       ‖adjointCarlesonSum ℭ f x₀‖ₑ + (ε / 2 : ℝ≥0) := by
     apply ENNReal.exists_biSup_le_enorm_add_eps (by positivity)
       ⟨c J, mem_ball_self (by unfold defaultD; positivity)⟩
-    rw [isBounded_image_iff_bddAbove_norm]
+    rw [isBounded_image_iff_bddAbove_norm']
     exact hf.bddAbove_norm_adjointCarlesonSum |>.mono (image_subset_range ..)
   obtain ⟨x', hx', ex'⟩ : ∃ x₀ ∈ ball (c J) (8⁻¹ * D ^ s J),
       ‖adjointCarlesonSum ℭ f x₀‖ₑ - (ε / 2 : ℝ≥0) ≤
@@ -1779,10 +1779,9 @@ lemma holder_correlation_tree (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u
               (edist x x' / D ^ s J) ^ (a : ℝ)⁻¹ / edist x x' ^ τ :=
             ENNReal.div_le_div_right (edist_holderFunction_le hu₁ hu₂ hu h2u hJ hf₁ hf₂ mx mx') _
           _ = _ := by
-            have dn0 : edist x x' ≠ 0 := by rw [← zero_lt_iff]; exact edist_pos.mpr hn
             rw [mul_div_assoc, defaultτ, ← ENNReal.div_rpow_of_nonneg _ _ (by positivity),
               div_eq_mul_inv, div_eq_mul_inv, ← mul_rotate _ (edist x x'),
-              ENNReal.inv_mul_cancel dn0 (edist_ne_top x x'), one_mul]
+              ENNReal.inv_mul_cancel (by positivity [edist_pos.mpr hn]) (edist_ne_top x x'), one_mul]
     _ ≤ C7_5_9s a * C7_5_10 a * P7_5_4 t u₁ u₂ f₁ f₂ J +
         ENNReal.ofReal (16 * D ^ s J) ^ τ *
         (I7_5_4 a * P7_5_4 t u₁ u₂ f₁ f₂ J * ((D : ℝ≥0∞) ^ s J)⁻¹ ^ (a : ℝ)⁻¹) := by

Carleson/ForestOperator/RemainingTiles.lean

@@ -258,7 +258,7 @@ lemma square_function_count (hJ : J ∈ 𝓙₆ t u₁) {s' : ℤ} :
     rw [Measure.restrict_apply_univ]
     exact volume_coeGrid_lt_top⟩
   let 𝒟 (s₀ x) : Set (Grid X) := { I | x ∈ ball (c I) (8 * D ^ s I) ∧ s I = s₀ }
-  let supp : Set X := { x ∈ J | EMetric.infEdist x Jᶜ ≤ 8 * (D ^ (s J - s')) }
+  let supp : Set X := { x ∈ J | Metric.infEDist x Jᶜ ≤ 8 * (D ^ (s J - s')) }
   have hsupp : supp ⊆ J := fun x hx ↦ hx.1
   have vsupp : volume.real supp ≤ 2 * (↑8 * ↑D ^ (-s')) ^ κ * volume.real (J : Set X) := by
     simp only [supp, sub_eq_neg_add, ENNReal.zpow_add (x := D) (by simp) (by finiteness),
@@ -361,13 +361,20 @@ lemma square_function_count (hJ : J ∈ 𝓙₆ t u₁) {s' : ℤ} :
   congr!
   simp [mul_assoc, mul_comm (G := ℝ) 14]
 
+-- PRed to mathlib: leanprover-community/mathlib4#34142
+variable {α} (s t : Finset α) in
+theorem _root_.Finset.diag_eq_filter [DecidableEq α] :
+    Finset.diag s = (s ×ˢ s).filter fun a : α × α => a.fst = a.snd := by
+  ext; simp +contextual
+
 open Classical in
 lemma sum_𝓙₆_indicator_sq_eq {f : Grid X → X → ℝ≥0∞} :
     (∑ J ∈ (𝓙₆ t u₁).toFinset, (J : Set X).indicator (f J) x) ^ 2 =
     ∑ J ∈ (𝓙₆ t u₁).toFinset, (J : Set X).indicator (f J · ^ 2) x := by
   rw [sq, Finset.sum_mul_sum, ← Finset.sum_product']
-  have dsub : (𝓙₆ t u₁).toFinset.diag ⊆ (𝓙₆ t u₁).toFinset ×ˢ (𝓙₆ t u₁).toFinset :=
-    Finset.filter_subset ..
+  have dsub : (𝓙₆ t u₁).toFinset.diag ⊆ (𝓙₆ t u₁).toFinset ×ˢ (𝓙₆ t u₁).toFinset := by
+    rw [Finset.diag_eq_filter]
+    exact Finset.filter_subset ..
   rw [← Finset.sum_subset dsub]; swap
   · intro p mp np
     simp_rw [Finset.mem_product, Finset.mem_diag, mem_toFinset, not_and] at mp np

Carleson/GridStructure.lean

@@ -35,7 +35,7 @@ class GridStructure {A : outParam ℝ≥0} [PseudoMetricSpace X] [DoublingMeasur
   ball_subset_Grid {i} : ball (c i) (D ^ s i / 4) ⊆ coeGrid i --2.0.10
   Grid_subset_ball {i} : coeGrid i ⊆ ball (c i) (4 * D ^ s i) --2.0.10
   small_boundary {i} {t : ℝ≥0} (ht : D ^ (- S - s i) ≤ t) :
-    volume.real { x ∈ coeGrid i | EMetric.infEdist x (coeGrid i)ᶜ ≤ t * (D ^ (s i):ℝ≥0∞)} ≤
+    volume.real { x ∈ coeGrid i | Metric.infEDist x (coeGrid i)ᶜ ≤ t * (D ^ (s i):ℝ≥0∞)} ≤
     2 * t ^ κ * volume.real (coeGrid i)
   coeGrid_measurable {i} : MeasurableSet (coeGrid i)
 

Carleson/TileExistence.lean

@@ -825,7 +825,7 @@ lemma dyadic_property {l : ℤ} (hl : -S ≤ l) {k : ℤ} (hl_k : l ≤ k) :
 structure ClosenessProperty {k1 k2 : ℤ} (hk1 : -S ≤ k1) (hk2 : -S ≤ k2)
     (y1 : Yk X k1) (y2 : Yk X k2) : Prop where
   I3_subset : I3 hk1 y1 ⊆ I3 hk2 y2
-  I3_infdist_lt : EMetric.infEdist (y1 : X) (I3 hk2 y2)ᶜ < (6 * D ^ k1 : ℝ≥0∞)
+  I3_infdist_lt : Metric.infEDist (y1 : X) (I3 hk2 y2)ᶜ < (6 * D ^ k1 : ℝ≥0∞)
 
 local macro "clProp(" hkl:term ", " y1:term " | " hkr:term ", " y2:term ")" : term =>
  `(ClosenessProperty $hkl $hkr $y1 $y2)
@@ -854,7 +854,7 @@ lemma transitive_boundary' {k1 k2 k3 : ℤ} (hk1 : -S ≤ k1) (hk2 : -S ≤ k2)
     exact (ENNReal.zpow_pos hd_nzero (by finiteness) _).ne'
   have hdp_finit42 : (D ^ 42 : ℝ≥0∞) ≠ ⊤ := by finiteness
   refine ⟨⟨hi3_1_2, ?_⟩, ⟨hi3_2_3, ?_⟩⟩
-  · apply lt_of_le_of_lt (EMetric.infEdist_anti _) hx'
+  · 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'
@@ -863,16 +863,16 @@ lemma transitive_boundary' {k1 k2 k3 : ℤ} (hk1 : -S ≤ k1) (hk2 : -S ≤ k2)
     rw [ENNReal.ofReal_mul (by norm_num), ← ENNReal.ofReal_rpow_of_pos (realD_pos a),
       ENNReal.ofReal_ofNat,ENNReal.ofReal_natCast,ENNReal.rpow_intCast] at hx_4k2 hx_4k2'
     calc
-      EMetric.infEdist (y2 : X) (I3 hk3 y3)ᶜ
-        ≤ edist (y2 : X) (y1 : X) + EMetric.infEdist (y1 : X) (I3 hk3 y3)ᶜ :=
-          EMetric.infEdist_le_edist_add_infEdist
-      _ = EMetric.infEdist (y1 : X) (I3 hk3 y3)ᶜ + edist (y1 : X) (y2 : X) := by
+      Metric.infEDist (y2 : X) (I3 hk3 y3)ᶜ
+        ≤ edist (y2 : X) (y1 : X) + Metric.infEDist (y1 : X) (I3 hk3 y3)ᶜ :=
+          Metric.infEDist_le_edist_add_infEDist
+      _ = Metric.infEDist (y1 : X) (I3 hk3 y3)ᶜ + edist (y1 : X) (y2 : X) := by
         rw [add_comm,edist_comm]
-      _ ≤ EMetric.infEdist (y1 : X) (I3 hk3 y3)ᶜ +
+      _ ≤ Metric.infEDist (y1 : X) (I3 hk3 y3)ᶜ +
           (edist (y1:X) x + edist x y2) := by
         rw [ENNReal.add_le_add_iff_left hx'.ne_top]
         exact edist_triangle (↑y1) x ↑y2
-      _ < EMetric.infEdist (y1 : X) (I3 hk3 y3)ᶜ + edist (y1 : X) x + 4 * D ^ k2 := by
+      _ < Metric.infEDist (y1 : X) (I3 hk3 y3)ᶜ + edist (y1 : X) x + 4 * D ^ k2 := by
         rw [← add_assoc, ENNReal.add_lt_add_iff_left (by finiteness)]
         exact hx_4k2
       _ < 6 * D ^ k1 + 4 * D ^ k1 + 4 * D ^ k2 := by
@@ -919,7 +919,7 @@ lemma transitive_boundary {k1 k2 k3 : ℤ} (hk1 : -S ≤ k1) (hk2 : -S ≤ k2) (
     · exact ⟨le_refl _,by
         obtain hx := hcl.I3_infdist_lt
         apply lt_of_le_of_lt _ hx
-        apply EMetric.infEdist_anti
+        apply Metric.infEDist_anti
         simp only [compl_subset_compl]
         exact hcl.I3_subset⟩
     exact hcl
@@ -1116,7 +1116,7 @@ lemma small_boundary' (k : ℤ) (hk : -S ≤ k) (hk_mK : -S ≤ k - K') (y : Yk
           simp only [disjoint_iUnion_right, disjoint_iUnion_left]
           intro u hu u' hu'
           rw [Set.disjoint_iff]
-          obtain ⟨x,hx⟩ := EMetric.infEdist_lt_iff.mp hu'.I3_infdist_lt
+          obtain ⟨x, hx⟩ := Metric.infEDist_lt_iff.mp hu'.I3_infdist_lt
           intro x' hx'
           have : x ∈ ball (u:X) (2⁻¹ * D^(l:ℤ)) := by
             simp only [mem_inter_iff, mem_compl_iff, mem_ball] at hx hx' ⊢
@@ -1411,7 +1411,7 @@ end ProofData
 
 lemma boundary_measure {k : ℤ} (hk : -S ≤ k) (y : Yk X k) {t : ℝ≥0} (ht : t ∈ Set.Ioo 0 1)
     (htD : (D ^ (-S : ℤ) : ℝ) ≤ t * D ^ k) :
-    volume ({x | x ∈ I3 hk y ∧ EMetric.infEdist x (I3 hk y)ᶜ ≤ (↑t * ↑D ^ k)}) ≤
+    volume ({x | x ∈ I3 hk y ∧ Metric.infEDist x (I3 hk y)ᶜ ≤ (↑t * ↑D ^ k)}) ≤
       2 * t ^ κ * volume (I3 hk y) := by
   have hconst_n : -S ≤ k - const_n a ht * K' := by
     suffices (D ^ (-S : ℤ) : ℝ) ≤ D ^ (k - const_n a ht * K' : ℤ) by
@@ -1425,7 +1425,7 @@ lemma boundary_measure {k : ℤ} (hk : -S ≤ k) (y : Yk X k) {t : ℝ≥0} (ht
     positivity
   simp only [mem_Ioo] at ht
   calc
-    volume ({x | x ∈ I3 hk y ∧ EMetric.infEdist x (I3 hk y)ᶜ ≤ (↑t * ↑D ^ k)})
+    volume ({x | x ∈ I3 hk y ∧ Metric.infEDist x (I3 hk y)ᶜ ≤ (↑t * ↑D ^ k)})
     _ ≤ volume (⋃ (y' : Yk X (k - const_n a ht *K')), ⋃ (_ : clProp(hconst_n,y'|hk,y)),
           I3 hconst_n y') := by
       apply volume.mono
@@ -1450,9 +1450,9 @@ lemma boundary_measure {k : ℤ} (hk : -S ≤ k) (y : Yk X k) {t : ℝ≥0} (ht
         rw [← ENNReal.ofReal_natCast,ENNReal.ofReal_pos]
         exact realD_pos a
       calc
-        EMetric.infEdist (y' : X) (I3 hk y)ᶜ
-        _ ≤ EMetric.infEdist (x:X) (I3 hk y)ᶜ + edist (y':X) x :=
-          EMetric.infEdist_le_infEdist_add_edist
+        Metric.infEDist (y' : X) (I3 hk y)ᶜ
+        _ ≤ Metric.infEDist (x:X) (I3 hk y)ᶜ + edist (y':X) x :=
+          Metric.infEDist_le_infEDist_add_edist
         _ < t * D^k + 4 * D^(k-const_n a ht * K') := by
           apply ENNReal.add_lt_add_of_le_of_lt _ hxb' hxy'
           apply (hxb'.trans_lt _).ne
@@ -1540,11 +1540,11 @@ lemma boundary_measure {k : ℤ} (hk : -S ≤ k) (y : Yk X k) {t : ℝ≥0} (ht
 
 lemma boundary_measure' {k : ℤ} (hk : -S ≤ k) (y : Yk X k) {t : ℝ≥0} (ht : t ∈ Set.Ioo 0 1)
     (htD : (D ^ (-S : ℤ) : ℝ) ≤ t * D ^ k) :
-    volume.real ({x | x ∈ I3 hk y ∧ EMetric.infEdist x (I3 hk y)ᶜ ≤ (↑t * ↑D ^ k)}) ≤
+    volume.real ({x | x ∈ I3 hk y ∧ Metric.infEDist x (I3 hk y)ᶜ ≤ (↑t * ↑D ^ k)}) ≤
       2 * t ^ κ * volume.real (I3 hk y) := by
   dsimp only [Measure.real]
   calc
-    volume ({x | x ∈ I3 hk y ∧ EMetric.infEdist x (I3 hk y)ᶜ ≤ (↑t * ↑D ^ k)}) |>.toReal
+    volume ({x | x ∈ I3 hk y ∧ Metric.infEDist x (I3 hk y)ᶜ ≤ (↑t * ↑D ^ k)}) |>.toReal
     _ ≤ ((2 : ℝ≥0∞) * t ^ κ : ℝ≥0∞).toReal * (volume (I3 hk y)).toReal := by
         rw [← ENNReal.toReal_mul]
         rw [ENNReal.toReal_le_toReal]