chore: bump mathlib to 4.19.0rc2 (#293)

Builds on #287 (but I couldn't push to this branch because I work from a
fork, hence the new PR).

The issue that #287 couldn't solve is solved here in an ugly way
(declaring an instance by hand with `letI`). Probably related to the new
structure elaboration. I'll report the difficulty on Zulip.

The file `MeasureReal` has been upstreamed, and is therefore deleted in
this PR. During the upstreaming, there was the comment that the `nnreal`
version had no API, and was probably not a good idea anyway, so it has
been deleted. This means that, in the project, I have replaced the lines
`volume.nnreal s` with `(volume s).toNNReal`. In most cases, these are
an indication that one should probably work with ENNReal instead (just
like we switched from NNNorm to ENorm), but I haven't made any such
change in the PR, which is a pure bump PR without any other change.

---------

Co-authored-by: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

Author: 3 people

Carleson.lean

@@ -46,7 +46,6 @@ import Carleson.ToMathlib.Data.ENNReal
 import Carleson.ToMathlib.DoublingMeasure
 import Carleson.ToMathlib.ENorm
 import Carleson.ToMathlib.HardyLittlewood
-import Carleson.ToMathlib.MeasureReal
 import Carleson.ToMathlib.MeasureTheory.Function.LpSeminorm.Basic
 import Carleson.ToMathlib.MeasureTheory.Integral.Lebesgue
 import Carleson.ToMathlib.MeasureTheory.Integral.MeanInequalities

Carleson/Antichain/AntichainOperator.lean

@@ -118,24 +118,24 @@ private lemma ineq_6_1_7 (x : X) {𝔄 : Set (𝔓 X)} (p : 𝔄) :
     _ = 2 ^ (5 * a + 101 * a ^ 3) / volume.real (ball x (8 * ↑D ^ 𝔰 p.1)) := by ring_nf
 
 private lemma ineq_6_1_7' (x : X) {𝔄 : Set (𝔓 X)} (p : 𝔄) :
-    (2 : ℝ≥0) ^ a ^ 3 / volume.nnreal (ball x (↑D ^ 𝔰 p.1 / (↑D * 4))) ≤
-      2 ^ (5 * a + 101 * a ^ 3) / volume.nnreal (ball x (8 * ↑D ^ 𝔰 p.1)) := by
+    (2 : ℝ≥0) ^ a ^ 3 / (volume (ball x (↑D ^ 𝔰 p.1 / (↑D * 4)))).toNNReal ≤
+      2 ^ (5 * a + 101 * a ^ 3) / (volume (ball x (8 * ↑D ^ 𝔰 p.1))).toNNReal := by
   suffices (2 : ℝ≥0) ^ a ^ 3 / volume.real (ball x (↑D ^ 𝔰 p.1 / (↑D * 4))) ≤
       2 ^ (5 * a + 101 * a ^ 3) / volume.real (ball x (8 * ↑D ^ 𝔰 p.1)) by
-    simp only [← NNReal.coe_le_coe, NNReal.coe_div, ← NNReal.val_eq_coe, measureNNReal_val]
+    simp only [← NNReal.coe_le_coe, NNReal.coe_div, ← NNReal.val_eq_coe]
     exact this
   exact ineq_6_1_7 x p
 
 -- Composition of inequalities 6.1.6, 6.1.7, 6.1.8.
 lemma norm_Ks_le' {x y : X} {𝔄 : Set (𝔓 X)} (p : 𝔄) (hxE : x ∈ E ↑p) (hy : Ks (𝔰 p.1) x y ≠ 0)  :
     ‖Ks (𝔰 p.1) x y‖₊ ≤
-      (2 : ℝ≥0) ^ (6*a + 101*a^3) / volume.nnreal (ball (𝔠 p.1) (8*D ^ 𝔰 p.1)) := by
+      (2 : ℝ≥0) ^ (6*a + 101*a^3) / (volume (ball (𝔠 p.1) (8*D ^ 𝔰 p.1))).toNNReal := by
   have hDpow_pos : 0 < (D : ℝ) ^ 𝔰 p.1 := defaultD_pow_pos ..
   have h8Dpow_pos : 0 < 8 * (D : ℝ) ^ 𝔰 p.1 := mul_defaultD_pow_pos _ (by linarith) _
   have hdist_cp : dist x (𝔠 p) ≤ 4*D ^ 𝔰 p.1 := le_of_lt (mem_ball.mp (Grid_subset_ball hxE.1))
-  have h : ‖Ks (𝔰 p.1) x y‖₊ ≤ (2 : ℝ≥0)^(a^3) / volume.nnreal (ball x (D ^ (𝔰 p.1 - 1)/4)) := by
+  have h : ‖Ks (𝔰 p.1) x y‖₊ ≤ (2 : ℝ≥0)^(a^3) / (volume (ball x (D ^ (𝔰 p.1 - 1)/4))).toNNReal := by
     apply le_trans (NNReal.coe_le_coe.mpr kernel_bound_old)
-    rw [NNReal.coe_div, NNReal.coe_pow, NNReal.coe_ofNat, ← NNReal.val_eq_coe, measureNNReal_val]
+    rw [NNReal.coe_div, NNReal.coe_pow, NNReal.coe_ofNat, ← NNReal.val_eq_coe]
     exact div_le_div_of_nonneg_left (pow_nonneg zero_le_two _)
       (measure_ball_pos_real x _ (div_pos (zpow_pos (defaultD_pos _) _) zero_lt_four))
       (measureReal_mono (Metric.ball_subset_ball (dist_mem_Icc_of_Ks_ne_zero hy).1)
@@ -149,8 +149,8 @@ lemma norm_Ks_le' {x y : X} {𝔄 : Set (𝔓 X)} (p : 𝔄) (hxE : x ∈ E ↑p
     ge_iff_le]
   rw [ha, pow_add _ (5 * a + 101 * a ^ 3) a, mul_assoc]
   apply mul_le_mul_of_nonneg_left _ (zero_le _)
-  suffices (volume.nnreal (ball (𝔠 p.1) (8 * ↑D ^ 𝔰 p.1))) ≤
-      2 ^ a * (volume.nnreal (ball x (8 * ↑D ^ 𝔰 p.1))) by
+  suffices (volume (ball (𝔠 p.1) (8 * ↑D ^ 𝔰 p.1))).toNNReal ≤
+      2 ^ a * (volume (ball x (8 * ↑D ^ 𝔰 p.1))).toNNReal by
     rw [le_mul_inv_iff₀, ← le_inv_mul_iff₀ , mul_comm _ (_^a), inv_inv]
     exact this
     · exact inv_pos.mpr (measure_ball_pos_nnreal _ _ h8Dpow_pos)
@@ -196,8 +196,8 @@ lemma MaximalBoundAntichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤
         exact mul_lt_mul_of_pos_right (by norm_num) (defaultD_pow_pos ..)
     -- 6.1.6, 6.1.7, 6.1.8
     have hKs : ∀ (y : X) (hy : Ks (𝔰 p.1) x y ≠ 0), ‖Ks (𝔰 p.1) x y‖₊ ≤
-        (2 : ℝ≥0) ^ (6*a + 101*a^3) / volume.nnreal (ball (𝔠 p.1) (8*D ^ 𝔰 p.1)) := fun y hy ↦
-      norm_Ks_le' _ hxE hy
+        (2 : ℝ≥0) ^ (6*a + 101*a^3) / (volume (ball (𝔠 p.1) (8*D ^ 𝔰 p.1))).toNNReal :=
+      fun y hy ↦ norm_Ks_le' _ hxE hy
     calc (‖∑ (p ∈ 𝔄), carlesonOn p f x‖₊ : ℝ≥0∞)
       = ↑‖carlesonOn p f x‖₊:= by rw [Finset.sum_eq_single_of_mem p.1 p.2 hne_p]
     _ ≤ ∫⁻ (y : X), ‖cexp (I * (↑((Q x) y) - ↑((Q x) x))) * Ks (𝔰 p.1) x y * f y‖ₑ := by
@@ -224,7 +224,7 @@ lemma MaximalBoundAntichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤
         exact hdist_cpy y hy.1
     _ ≤ ∫⁻ (y : X) in ball (𝔠 ↑p) (8 * ↑D ^ 𝔰 p.1),
         (((2 : ℝ≥0) ^ (6*a + 101*a^3) /
-          volume.nnreal (ball (𝔠 p.1) (8*D ^ 𝔰 p.1))) * ‖f y‖₊ : ℝ≥0) := by
+          (volume (ball (𝔠 p.1) (8*D ^ 𝔰 p.1))).toNNReal) * ‖f y‖₊ : ℝ≥0) := by
       refine lintegral_mono_nnreal fun y ↦ ?_
       rw [nnnorm_mul]
       gcongr
@@ -236,7 +236,7 @@ lemma MaximalBoundAntichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤
       rw [laverage_eq, Measure.restrict_apply MeasurableSet.univ, univ_inter]
       simp_rw [div_eq_mul_inv, coe_mul, enorm_eq_nnnorm]
       rw [lintegral_const_mul _ hfm.nnnorm.coe_nnreal_ennreal, ENNReal.coe_pow, coe_inv
-        (ne_of_gt (measure_ball_pos_nnreal _ _ h8Dpow_pos)), measureNNReal_def,
+        (ne_of_gt (measure_ball_pos_nnreal _ _ h8Dpow_pos)),
         ENNReal.coe_toNNReal (measure_ball_ne_top _ _)]
       ring
     _ ≤ (C_6_1_2 a) * (ball (𝔠 p.1) (8*D ^ 𝔰 p.1)).indicator (x := x)

Carleson/Antichain/TileCorrelation.lean

@@ -353,16 +353,16 @@ open GridStructure
 -- Lemma 6.1.5 (part I)
 lemma correlation_le {p p' : 𝔓 X} (hle : 𝔰 p' ≤ 𝔰 p) {g : X → ℂ} (hg : Measurable g)
     (hg1 : ∀ x, ‖g x‖ ≤ G.indicator 1 x) :
-    ‖ ∫ y, (adjointCarleson p' g y) * conj (adjointCarleson p g y) ‖₊ ≤
-      (C_6_1_5 a) * ((1 + dist_(p') (𝒬 p') (𝒬 p))^(-(1 : ℝ)/(2*a^2 + a^3))) /
-        (volume.nnreal (coeGrid (𝓘 p))) * ∫ y in E p', ‖ g y‖ * ∫ y in E p, ‖ g y‖ := by
+    ‖∫ y, (adjointCarleson p' g y) * conj (adjointCarleson p g y)‖ₑ ≤
+      (C_6_1_5 a) * ((1 + nndist_(p') (𝒬 p') (𝒬 p))^(-(1 : ℝ)/(2*a^2 + a^3))) /
+        (volume (coeGrid (𝓘 p))) * ∫⁻ y in E p', ‖g y‖ₑ * ∫⁻ y in E p, ‖g y‖ₑ := by
   sorry
 
 -- Lemma 6.1.5 (part II)
 lemma correlation_zero_of_ne_subset {p p' : 𝔓 X} (hle : 𝔰 p' ≤ 𝔰 p) {g : X → ℂ}
     (hg : Measurable g) (hg1 : ∀ x, ‖g x‖ ≤ G.indicator 1 x)
     (hpp' : ¬ coeGrid (𝓘 p) ⊆ ball (𝔠 p) (15 * ↑D ^𝔰 p) ) :
-    ‖ ∫ y, (adjointCarleson p' g y) * conj (adjointCarleson p g y) ‖₊ = 0 := by
+    ‖∫ y, (adjointCarleson p' g y) * conj (adjointCarleson p g y)‖ₑ = 0 := by
   by_contra h0
   apply hpp'
   have hy : ∃ y : X, (adjointCarleson p' g y) * conj (adjointCarleson p g y) ≠ 0 := sorry

Carleson/Calculations.lean

@@ -128,7 +128,7 @@ lemma calculation_5 {dist_1 dist_2: ℝ}
     ← mul_assoc,
     neg_mul,
     Real.rpow_neg (by positivity),
-    LinearOrderedField.mul_inv_cancel (a := (2 : ℝ) ^ (100 * (a : ℝ))) (by positivity),
+    mul_inv_cancel₀ (a := (2 : ℝ) ^ (100 * (a : ℝ))) (by positivity),
     ← mul_assoc,
     ← Real.rpow_add (by positivity)
   ]

Carleson/Classical/CarlesonOnTheRealLine.lean

@@ -369,6 +369,7 @@ instance compatibleFunctions_R : CompatibleFunctions ℝ ℝ (2 ^ 4) where
   eq_zero := by
     use 0
     intro f
+    change f 0 = 0
     rw [coeΘ_R, mul_zero]
   localOscillation_le_cdist := oscillation_control
   cdist_mono := frequency_monotone

Carleson/Classical/DirichletKernel.lean

@@ -144,6 +144,7 @@ lemma dirichletKernel_eq_ae : ∀ᵐ (x : ℝ), dirichletKernel N x = dirichletK
     rw [ne_eq, mul_assoc, mul_assoc, mul_eq_mul_left_iff]
     simp only [I_ne_zero, or_false]
     norm_cast
+    ring_nf
     exact (h n).symm
   rw [ae_iff]
   apply measure_mono_null this

Carleson/Classical/Helper.lean

@@ -2,7 +2,7 @@
    one or they might be candidates to go there, possibly in a generalized form. -/
 
 import Carleson.ToMathlib.Misc
-import Mathlib.MeasureTheory.Integral.IntervalIntegral
+import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
 
 open MeasureTheory
 
@@ -80,14 +80,16 @@ lemma ConditionallyCompleteLattice.le_biSup {α : Type*} [ConditionallyCompleteL
 
 /- Adapted from mathlib Function.Periodic.exists_mem_Ico₀ -/
 theorem Function.Periodic.exists_mem_Ico₀' {α β : Type*} {f : α → β} {c : α}
-    [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c) (hc : 0 < c) (x : α) :
+    [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α]
+    (h : Periodic f c) (hc : 0 < c) (x : α) :
     ∃ (n : ℤ), (x - n • c) ∈ Set.Ico 0 c ∧ f x = f (x - n • c) :=
   let ⟨n, H, _⟩ := existsUnique_zsmul_near_of_pos' hc x
   ⟨n, H, (h.sub_zsmul_eq n).symm⟩
 
 /- Adapted from mathlib Function.Periodic.exists_mem_Ico₀ -/
 theorem Function.Periodic.exists_mem_Ico' {α β : Type*} {f : α → β} {c : α}
-    [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c) (hc : 0 < c) (x a: α) :
+    [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α]
+    (h : Periodic f c) (hc : 0 < c) (x a: α) :
     ∃ (n : ℤ), (x - n • c) ∈ Set.Ico a (a + c) ∧ f x = f (x - n • c) :=
   let ⟨n, H, _⟩ := existsUnique_sub_zsmul_mem_Ico hc x a
   ⟨n, H, (h.sub_zsmul_eq n).symm⟩

Carleson/Defs.lean

@@ -94,7 +94,7 @@ notation3 "ball_{" x " ," r "}" => @ball (WithFunctionDistance x r) _ in
 /-- A set `Θ` of (continuous) functions is compatible. `A` will usually be `2 ^ a`. -/
 class CompatibleFunctions (𝕜 : outParam Type*) (X : Type u) (A : outParam ℕ)
   [RCLike 𝕜] [PseudoMetricSpace X] extends FunctionDistances 𝕜 X where
-  eq_zero : ∃ o : X, ∀ f : Θ, f o = 0
+  eq_zero : ∃ o : X, ∀ f : Θ, coeΘ f o = 0
   /-- The distance is bounded below by the local oscillation. (1.0.7) -/
   localOscillation_le_cdist {x : X} {r : ℝ} {f g : Θ} :
     localOscillation (ball x r) (coeΘ f) (coeΘ g) ≤ ENNReal.ofReal (dist_{x, r} f g)

Carleson/Forest.lean

@@ -30,15 +30,15 @@ structure Forest (n : ℕ) where
   𝔘 : Set (𝔓 X)
   /-- The value of `𝔗 u` only matters when `u ∈ 𝔘`. -/
   𝔗 : 𝔓 X → Set (𝔓 X)
-  nonempty' {u} (hu : u ∈ 𝔘) : (𝔗 u).Nonempty
-  ordConnected' {u} (hu : u ∈ 𝔘) : OrdConnected (𝔗 u) -- (2.0.33)
-  𝓘_ne_𝓘' {u} (hu : u ∈ 𝔘) {p} (hp : p ∈ 𝔗 u) : 𝓘 p ≠ 𝓘 u
-  smul_four_le' {u} (hu : u ∈ 𝔘) {p} (hp : p ∈ 𝔗 u) : smul 4 p ≤ smul 1 u -- (2.0.32)
-  stackSize_le' {x} : stackSize 𝔘 x ≤ 2 ^ n -- (2.0.34), we formulate this a bit differently.
-  dens₁_𝔗_le' {u} (hu : u ∈ 𝔘) : dens₁ (𝔗 u) ≤ 2 ^ (4 * (a : ℝ) - n + 1) -- (2.0.35)
-  lt_dist' {u u'} (hu : u ∈ 𝔘) (hu' : u' ∈ 𝔘) (huu' : u ≠ u') {p} (hp : p ∈ 𝔗 u')
+  nonempty' {u : _} (hu : u ∈ 𝔘) : (𝔗 u).Nonempty
+  ordConnected' {u : _} (hu : u ∈ 𝔘) : OrdConnected (𝔗 u) -- (2.0.33)
+  𝓘_ne_𝓘' {u : _} (hu : u ∈ 𝔘) {p} (hp : p ∈ 𝔗 u) : 𝓘 p ≠ 𝓘 u
+  smul_four_le' {u : _} (hu : u ∈ 𝔘) {p} (hp : p ∈ 𝔗 u) : smul 4 p ≤ smul 1 u -- (2.0.32)
+  stackSize_le' {x : _} : stackSize 𝔘 x ≤ 2 ^ n -- (2.0.34), we formulate this a bit differently.
+  dens₁_𝔗_le' {u : _} (hu : u ∈ 𝔘) : dens₁ (𝔗 u) ≤ 2 ^ (4 * (a : ℝ) - n + 1) -- (2.0.35)
+  lt_dist' {u u' : _} (hu : u ∈ 𝔘) (hu' : u' ∈ 𝔘) (huu' : u ≠ u') {p} (hp : p ∈ 𝔗 u')
     (h : 𝓘 p ≤ 𝓘 u) : 2 ^ (Z * (n + 1)) < dist_(p) (𝒬 p) (𝒬 u) -- (2.0.36)
-  ball_subset' {u} (hu : u ∈ 𝔘) {p} (hp : p ∈ 𝔗 u) : ball (𝔠 p) (8 * D ^ 𝔰 p) ⊆ 𝓘 u -- (2.0.37)
+  ball_subset' {u : _} (hu : u ∈ 𝔘) {p} (hp : p ∈ 𝔗 u) : ball (𝔠 p) (8 * D ^ 𝔰 p) ⊆ 𝓘 u -- (2.0.37)
 
 namespace Forest
 

Carleson/Psi.lean

@@ -288,7 +288,7 @@ lemma support_ψS_subset_Icc {b c : ℤ} {x : ℝ}
   simp only [support_ψS hD hx, nonzeroS, Finset.coe_Icc, mem_Icc] at hi
   simp only [toFinset_Icc, Finset.coe_Icc, mem_Icc]
   refine ⟨le_trans ?_ hi.1, le_trans hi.2 ?_⟩
-  · rw [← Nat.cast_one, Int.floor_nat_add, Nat.cast_one, ← sub_le_iff_le_add', Int.le_floor,
+  · rw [← Nat.cast_one, Int.floor_natCast_add, Nat.cast_one, ← sub_le_iff_le_add', Int.le_floor,
       Real.le_logb_iff_rpow_le hD (mul_pos two_pos hx), mul_comm]
     exact_mod_cast (div_le_iff₀ two_pos).mp h.1
   · rw [Int.ceil_le, Real.logb_le_iff_le_rpow hD (mul_pos four_pos hx), mul_comm]
@@ -374,7 +374,7 @@ def D2_1_3 (a : ℝ≥0) : ℝ≥0 := 2 ^ (150 * (a : ℝ) ^ 3)
 
 /-- preferably use `kernel_bound` instead. -/
 lemma kernel_bound_old {s : ℤ} {x y : X} :
-    ‖Ks s x y‖₊ ≤ 2 ^ a ^ 3 / volume.nnreal (ball x (dist x y)) := by
+    ‖Ks s x y‖₊ ≤ 2 ^ a ^ 3 / (volume (ball x (dist x y))).toNNReal := by
   change ‖K x y * ψ (D ^ (-s) * dist x y)‖ ≤ 2 ^ a ^ 3 / volume.real (ball x (dist x y))
   apply le_trans <| calc
     ‖K x y * ψ (D ^ (-s) * dist x y)‖
@@ -416,7 +416,8 @@ private lemma DoublingMeasure.volume_ball_two_le_same_repeat' (x : X) (n : ℕ)
   field_simp
   ring
 
-lemma Metric.measure_ball_pos_nnreal (x : X) (r : ℝ) (hr : r > 0) : volume.nnreal (ball x r) > 0 :=
+lemma Metric.measure_ball_pos_nnreal (x : X) (r : ℝ) (hr : r > 0) :
+    (volume (ball x r)).toNNReal > 0 :=
   ENNReal.toNNReal_pos (ne_of_gt (measure_ball_pos volume x hr)) (measure_ball_ne_top x _)
 
 lemma Metric.measure_ball_pos_real (x : X) (r : ℝ) (hr : r > 0) : volume.real (ball x r) > 0 :=
@@ -453,7 +454,7 @@ private lemma div_vol_le {x y : X} {c : ℝ} (hc : c > 0) (hxy : dist x y ≥ D
   apply le_trans <| (div_le_div_iff_of_pos_left hc v0₁ v0₂).2 <|
     ENNReal.toNNReal_mono (measure_ball_ne_top x _) (OuterMeasureClass.measure_mono _ ball_subset)
   dsimp only
-  rw [measureNNReal_val, div_le_div_iff₀ (by exact_mod_cast v0₂) v0₃]
+  rw [div_le_div_iff₀ (by exact_mod_cast v0₂) v0₃]
   apply le_of_le_of_eq <| (mul_le_mul_left hc).2 <|
     DoublingMeasure.volume_ball_two_le_same_repeat' s x n
   simp_rw [defaultA, ← mul_assoc, mul_comm c]