define vol in ENNReal (#260)

* Define `vol` in the root namespace that lives in `ENNReal`. `Real.vol`
is still available.
* put `C_K` in `NNReal`
* prove `ENNReal`-versions of the `IsOneSidedKernel`-axioms. Replace the
axiom in `IsTwoSidedKernel` with its `ENNReal` version. (Doing that for
`IsOneSidedKernel` is a todo.)
* Prove `ENNReal` version of `kernel_bound`. (The old version is
`kernel_bound_old`.)

Author: fpvandoorn

Carleson/Antichain/AntichainOperator.lean

@@ -146,7 +146,7 @@ lemma norm_Ks_le' {x y : X} {𝔄 : Set (𝔓 X)} (p : 𝔄) (hxE : x ∈ E ↑p
   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
-    apply le_trans (NNReal.coe_le_coe.mpr kernel_bound)
+    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]
     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))

Carleson/Classical/CarlesonOnTheRealLine.lean

@@ -486,12 +486,24 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
     norm_cast
 
 
+-- remove?
 lemma Real.vol_real_eq {x y : ℝ} : Real.vol x y = 2 * |x - y| := by
-  rw [Real.vol, measureReal_def, Real.dist_eq, Real.volume_ball, ENNReal.toReal_ofReal (by linarith [abs_nonneg (x-y)])]
+  rw [Real.vol, measureReal_def, Real.dist_eq, Real.volume_ball,
+    ENNReal.toReal_ofReal (by linarith [abs_nonneg (x-y)])]
 
+-- proof can be simplified with enorm lemma
+lemma Real.vol_eq {x y : ℝ} : vol x y = 2 * ‖x - y‖ₑ := by
+  rw [vol, Real.volume_ball, ofReal_mul (by positivity), ← edist_dist, edist_eq_enorm_sub,
+    ofReal_ofNat]
+
+-- remove?
 lemma Real.vol_real_symm {x y : ℝ} : Real.vol x y = Real.vol y x := by
   rw [Real.vol_real_eq, Real.vol_real_eq, abs_sub_comm]
 
+-- proof can be simplified with enorm lemma
+lemma Real.vol_symm {x y : ℝ} : vol x y = vol y x := by
+  simp_rw [Real.vol_eq, ← ofReal_norm, norm_sub_rev]
+
 instance isOneSidedKernelHilbert : IsOneSidedKernel 4 K where
   /- uses Hilbert_kernel_bound -/
   norm_K_le_vol_inv := by
@@ -529,11 +541,11 @@ instance isOneSidedKernelHilbert : IsOneSidedKernel 4 K where
 instance isTwoSidedKernelHilbert : IsTwoSidedKernel 4 K where
   norm_K_sub_le' := by
     intro x x' y h
-    rw [Hilbert_kernel_conj_symm, @Hilbert_kernel_conj_symm y x', ← map_sub, Complex.norm_conj,
-      dist_comm x y, Real.vol_real_symm]
     rw [dist_comm x y] at h
-    exact isOneSidedKernelHilbert.norm_K_sub_le h
-#synth DoublingMeasure ℝ _
+    rw [Hilbert_kernel_conj_symm, @Hilbert_kernel_conj_symm y x', ← map_sub, ← ofReal_norm,
+      Complex.norm_conj, edist_comm x y, Real.vol_symm, ofReal_norm_eq_enorm]
+    exact enorm_K_sub_le (K := K) h
+
 local notation "T" => carlesonOperatorReal K
 
 --TODO : change name to reflect that this only holds for a specific instance of CarlesonOperaterReal?

Carleson/Defs.lean

@@ -1,11 +1,12 @@
 import Carleson.ToMathlib.DoublingMeasure
 import Carleson.ToMathlib.WeakType
+import Carleson.ToMathlib.Data.ENNReal
 import Mathlib.Algebra.Order.Group.Int
 import Mathlib.Analysis.CStarAlgebra.Classes
 import Mathlib.Data.Int.Star
 
-open MeasureTheory Measure NNReal Metric Complex Set TopologicalSpace Bornology Function
-open scoped ENNReal
+open MeasureTheory Measure Metric Complex Set TopologicalSpace Bornology Function ENNReal
+open scoped NNReal
 noncomputable section
 
 -- todo: rename and protect `Real.RCLike`
@@ -173,11 +174,24 @@ class IsCancellative (τ : ℝ) [CompatibleFunctions ℝ X A] : Prop where
 
 export IsCancellative (norm_integral_exp_le)
 
-/-- The "volume function" `V`. Note that we will need to assume
-`IsFiniteMeasureOnCompacts` and `ProperSpace` to actually know that this volume is finite. -/
-def Real.vol {X : Type*} [PseudoMetricSpace X] [MeasureSpace X] (x y : X) : ℝ :=
+/-- The "volume function" `V`. Preferably use `vol` instead. -/
+protected def Real.vol {X : Type*} [PseudoMetricSpace X] [MeasureSpace X] (x y : X) : ℝ :=
   volume.real (ball x (dist x y))
 
+/-- The "volume function" `V`. We will need to assume
+`IsFiniteMeasureOnCompacts` and `ProperSpace` to actually know that this volume is finite. -/
+def vol {X : Type*} [PseudoMetricSpace X] [MeasureSpace X] (x y : X) : ℝ≥0∞ :=
+  volume (ball x (dist x y))
+
+lemma Real.vol_def {X : Type*} [PseudoMetricSpace X] [MeasureSpace X] {x y : X} :
+  Real.vol x y = (vol x y).toReal := rfl
+
+lemma ofReal_vol {X : Type*} [PseudoMetricSpace X] [MeasureSpace X] [ProperSpace X]
+  [IsFiniteMeasureOnCompacts (volume : Measure X)] {x y : X} :
+    ENNReal.ofReal (Real.vol x y) = vol x y := by
+  simp_rw [Real.vol_def, ENNReal.ofReal_toReal_eq_iff, vol]
+  apply measure_ball_ne_top
+
 -- /-- In Mathlib we only have the operator norm for continuous linear maps,
 -- and `T_*` is not linear.
 -- Here is the norm for an arbitrary map `T` between normed spaces
@@ -245,22 +259,24 @@ lemma mul_defaultD_pow_pos (a : ℕ) {r : ℝ} (hr : 0 < r) (z : ℤ) : 0 < r *
 section Kernel
 
 variable {X : Type*} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [MeasureSpace X]
-open Real (vol)
 open Function
 
 /-- The constant used twice in the definition of the Calderon-Zygmund kernel. -/
-@[simp] def C_K (a : ℝ) : ℝ := 2 ^ a ^ 3
+@[simp] def C_K (a : ℝ) : ℝ≥0 := 2 ^ a ^ 3
 
-lemma C_K_pos (a : ℝ) : 0 < C_K a := by unfold C_K; positivity
+lemma C_K_pos {a : ℝ} : 0 < C_K a := NNReal.rpow_pos (by norm_num)
+lemma C_K_pos_real {a : ℝ} : 0 < (C_K a : ℝ) := C_K_pos
 
 /-- `K` is a one-sided Calderon-Zygmund kernel
 In the formalization `K x y` is defined everywhere, even for `x = y`. The assumptions on `K` show
-that `K x x = 0`. -/
+that `K x x = 0`.
+
+Todo: maybe make enorm_K_le_vol_inv + enorm_K_sub_le + K_eq_zero_of_dist_eq_zero the axioms. -/
 class IsOneSidedKernel (a : outParam ℕ) (K : X → X → ℂ) : Prop where
   measurable_K : Measurable (uncurry K)
-  norm_K_le_vol_inv (x y : X) : ‖K x y‖ ≤ C_K a / vol x y
+  norm_K_le_vol_inv (x y : X) : ‖K x y‖ ≤ C_K a / Real.vol x y
   norm_K_sub_le {x y y' : X} (h : 2 * dist y y' ≤ dist x y) :
-    ‖K x y - K x y'‖ ≤ (dist y y' / dist x y) ^ (a : ℝ)⁻¹ * (C_K a / vol x y)
+    ‖K x y - K x y'‖ ≤ (dist y y' / dist x y) ^ (a : ℝ)⁻¹ * (C_K a / Real.vol x y)
 
 export IsOneSidedKernel (measurable_K norm_K_le_vol_inv norm_K_sub_le)
 
@@ -278,27 +294,47 @@ lemma measurable_K_left [IsOneSidedKernel a K] (y : X) : Measurable (K · y) :=
 lemma measurable_K_right [IsOneSidedKernel a K] (x : X) : Measurable (K x) :=
   measurable_K.of_uncurry_left
 
-lemma integrableOn_K_Icc [IsOpenPosMeasure (volume : Measure X)] [ProperSpace X]
+lemma enorm_K_le_vol_inv [ProperSpace X] [IsFiniteMeasureOnCompacts (volume : Measure X)]
+    [IsOneSidedKernel a K] (x y : X) : ‖K x y‖ₑ ≤ (C_K a : ℝ≥0∞) / vol x y := by
+  rw [← ofReal_norm, ← ofReal_vol, ← ofReal_coe_nnreal]
+  refine le_trans ?_ (ofReal_div_le measureReal_nonneg)
+  gcongr
+  apply norm_K_le_vol_inv
+
+
+lemma enorm_K_sub_le [ProperSpace X] [IsFiniteMeasureOnCompacts (volume : Measure X)]
+    [IsOneSidedKernel a K] {x y y' : X} (h : 2 * dist y y' ≤ dist x y) :
+    ‖K x y - K x y'‖ₑ ≤ (edist y y' / edist x y) ^ (a : ℝ)⁻¹ * (C_K a / vol x y) := by
+  simp_rw [← ofReal_norm, ← ofReal_vol, ← ofReal_coe_nnreal, edist_dist]
+  calc
+    _ ≤ ENNReal.ofReal ((dist y y' / dist x y) ^ (a : ℝ)⁻¹ * (C_K a / Real.vol x y)) := by
+      gcongr; apply norm_K_sub_le h
+    _ ≤ _ := by
+      rw [ENNReal.ofReal_mul']; swap
+      · exact div_nonneg NNReal.zero_le_coe measureReal_nonneg
+      gcongr
+      · rw [← ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity)]
+        gcongr
+        apply ofReal_div_le (by positivity)
+      · exact ofReal_div_le measureReal_nonneg
+
+lemma integrableOn_K_Icc [IsOpenPosMeasure (volume : Measure X)]
+    [IsFiniteMeasureOnCompacts (volume : Measure X)] [ProperSpace X]
     [Regular (volume : Measure X)] [IsOneSidedKernel a K] {x : X} {r R : ℝ} (hr : r > 0) :
     IntegrableOn (K x) {y | dist x y ∈ Icc r R} volume := by
   use Measurable.aestronglyMeasurable (measurable_K_right x)
   rw [hasFiniteIntegral_def]
   calc ∫⁻ (y : X) in {y | dist x y ∈ Icc r R}, ‖K x y‖ₑ
-    _ ≤ ∫⁻ (y : X) in {y | dist x y ∈ Icc r R},
-          ENNReal.ofReal (C_K a / volume.real (ball x r)) := by
+    _ ≤ ∫⁻ (y : X) in {y | dist x y ∈ Icc r R}, C_K a / volume (ball x r) := by
       refine setLIntegral_mono measurable_const (fun y hy ↦ ?_)
-      rw [← ofReal_norm]
-      refine ENNReal.ofReal_le_ofReal <| (norm_K_le_vol_inv x y).trans ?_
+      refine (enorm_K_le_vol_inv x y).trans ?_
+      rw [vol]
       gcongr
-      · exact (C_K_pos a).le
-      · rw [measureReal_def]
-        apply ENNReal.toReal_pos (ne_of_gt <| measure_ball_pos volume x hr)
-        exact measure_ball_ne_top x r
-      · exact measureReal_mono (ball_subset_ball hy.1)
+      exact hy.1
     _ < _ := by
-      rw [lintegral_const]
-      apply ENNReal.mul_lt_top ENNReal.ofReal_lt_top
-      rw [Measure.restrict_apply MeasurableSet.univ, univ_inter]
+      rw [setLIntegral_const]
+      apply ENNReal.mul_lt_top (ENNReal.div_lt_top ENNReal.coe_ne_top _); swap
+      · simp_rw [← pos_iff_ne_zero, measure_ball_pos _ _ hr]
       refine (Ne.lt_top fun h ↦ ?_)
       have : {y | dist x y ∈ Icc r R} ⊆ closedBall x R := by
         intro y ⟨_, hy⟩
@@ -310,7 +346,7 @@ In the formalization `K x y` is defined everywhere, even for `x = y`. The assump
 that `K x x = 0`. -/
 class IsTwoSidedKernel (a : outParam ℕ) (K : X → X → ℂ) extends IsOneSidedKernel a K where
   norm_K_sub_le' {x x' y : X} (h : 2 * dist x x' ≤ dist x y) :
-    ‖K x y - K x' y‖ ≤ (dist x x' / dist x y) ^ (a : ℝ)⁻¹ * (C_K a / vol x y)
+    ‖K x y - K x' y‖ₑ ≤ (edist x x' / edist x y) ^ (a : ℝ)⁻¹ * (C_K a / vol x y)
 
 export IsTwoSidedKernel (norm_K_sub_le')
 
@@ -364,7 +400,7 @@ lemma le_cdist_iterate {x : X} {r : ℝ} (hr : 0 ≤ r) (f g : Θ X) (k : ℕ) :
   | succ k ih =>
     trans 2 * dist_{x, (defaultA a) ^ k * r} f g
     · rw [pow_succ', mul_assoc]
-      exact (mul_le_mul_left zero_lt_two).mpr ih
+      exact (_root_.mul_le_mul_left zero_lt_two).mpr ih
     · convert le_cdist (ball_subset_ball _) using 1
       · exact dist_congr rfl (by rw [← mul_assoc, pow_succ'])
       · nth_rw 1 [← one_mul ((defaultA a) ^ k * r)]; gcongr

Carleson/Psi.lean

@@ -369,8 +369,8 @@ def C2_1_3 (a : ℝ≥0) : ℝ≥0 := 2 ^ (102 * (a : ℝ) ^ 3)
 /-- The constant appearing in part 3 of Lemma 2.1.3. -/
 def D2_1_3 (a : ℝ≥0) : ℝ≥0 := 2 ^ (150 * (a : ℝ) ^ 3)
 
---1.0.14.
-lemma kernel_bound {s : ℤ} {x y : X} :
+/-- 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
   change ‖K x y * ψ (D ^ (-s) * dist x y)‖ ≤ 2 ^ a ^ 3 / volume.real (ball x (dist x y))
   apply le_trans <| calc
@@ -382,6 +382,17 @@ lemma kernel_bound {s : ℤ} {x y : X} :
   unfold C_K
   norm_cast
 
+-- 1.0.14.
+lemma kernel_bound {s : ℤ} {x y : X} : ‖Ks s x y‖ₑ ≤ C_K a / vol x y := by
+  change ‖K x y * ψ (D ^ (-s) * dist x y)‖ₑ ≤ C_K a / volume (ball x (dist x y))
+  calc
+    ‖K x y * ψ (D ^ (-s) * dist x y)‖ₑ
+      = ‖K x y‖ₑ * ‖(ψ (D ^ (-s) * dist x y) : ℂ)‖ₑ := enorm_mul ..
+    _ ≤ ‖K x y‖ₑ * 1               := by
+        gcongr; rw [← ofReal_norm, norm_real]; norm_cast; exact abs_ψ_le_one D _
+    _ ≤ ‖K x y‖ₑ                   := by rw [mul_one]
+    _ ≤ _ := enorm_K_le_vol_inv x y
+
 variable (s)
 
 /-- Apply `volume_ball_two_le_same` `n` times. -/
@@ -411,17 +422,20 @@ lemma Metric.measure_ball_pos_real (x : X) (r : ℝ) (hr : r > 0) : volume.real
 include a q K σ₁ σ₂ F G in
 lemma K_eq_K_of_dist_eq_zero {x y y' : X} (hyy' : dist y y' = 0) :
     K x y = K x y' := by
-  suffices ‖K x y - K x y'‖ = 0 by rwa [norm_sub_eq_zero_iff] at this
-  suffices ‖K x y - K x y'‖ ≤ 0 from le_antisymm this (norm_nonneg (K x y - K x y'))
-  convert norm_K_sub_le (K := K) (x := x) (y := y) (y' := y')
+  suffices ‖K x y - K x y'‖ₑ = 0 by rwa [enorm_eq_zero, sub_eq_zero] at this
+  suffices ‖K x y - K x y'‖ₑ ≤ 0 from le_antisymm this (zero_le _)
+  convert enorm_K_sub_le (K := K) (x := x) (y := y) (y' := y')
     (by simp only [hyy', mul_zero, dist_nonneg])
-  suffices (0 : ℝ) ^ (a : ℝ)⁻¹ = 0 by simp [hyy', this]
-  simp [inv_ne_zero (show (a : ℝ) ≠ 0 by norm_cast; linarith [four_le_a X])]
+  replace hyy' : edist y y' = 0 := by rw [edist_dist, hyy', ENNReal.ofReal_zero]
+  suffices (0 : ℝ≥0∞) ^ (a : ℝ)⁻¹ = 0 by simp [hyy', this]
+  have : 0 < a := by linarith [four_le_a X]
+  simp [this]
 
 include a q K σ₁ σ₂ F G in
 lemma K_eq_zero_of_dist_eq_zero {x y : X} (hxy : dist x y = 0) :
     K x y = 0 :=
-  norm_le_zero_iff.1 (by simpa [hxy, Real.vol] using norm_K_le_vol_inv x y)
+  norm_le_zero_iff.1 <| by
+    simpa [hxy, Real.vol, ENNReal.div_zero] using norm_K_le_vol_inv (K := K) x y
 
 variable {s}
 
@@ -450,13 +464,14 @@ private lemma div_vol_le₀ {x y : X} {c : ℝ} (hc : c > 0) (hK : Ks s x y ≠
     (2 ^ (2 * a + 100 * a ^ 3)) * c / volume.real (ball x (D ^ s)) := by
   simpa using div_vol_le hc (mem_Icc.1 (dist_mem_Icc_of_Ks_ne_zero hK)).1 0
 
+-- preferably use `enorm_K_le`
 lemma norm_K_le {s : ℤ} {x y : X} (n : ℕ) (hxy : dist x y ≥ D ^ (s - 1) / 4) :
     ‖K x y‖ ≤ 2 ^ ((2 + n) * (a : ℝ) + 101 * a ^ 3) / volume.real (ball x (2 ^ n * D ^ s)) := by
   by_cases h : dist x y = 0
   · rw [K_eq_zero_of_dist_eq_zero h, norm_zero]; positivity
   apply (norm_K_le_vol_inv x y).trans
   unfold C_K
-  apply le_trans (div_vol_le (by positivity) hxy n)
+  apply le_trans (div_vol_le (by norm_cast; positivity) hxy n)
   apply div_le_div_of_nonneg_right _ measureReal_nonneg
   exact_mod_cast le_of_eq (by ring)
 
@@ -616,7 +631,6 @@ private lemma norm_Ks_sub_Ks_le₀₀ {s : ℤ} {x y y' : X} (hK : Ks s x y ≠
      (hyy' : 2 * dist y y' ≤ dist x y) : ‖K x y - K x y'‖ * |ψ (D ^ (-s) * dist x y')| ≤
     (2 : ℝ) ^ (1 + 102 * a + 101 * a ^ 3) / volume.real (ball x (D ^ s)) *
     (dist y y' / D ^ s) ^ (a : ℝ)⁻¹ := by
-  have CKa0 : C_K a > 0 := by unfold C_K; positivity
   have D1 := D1 X
   have d0 : dist x y > 0 :=
     lt_of_lt_of_le (by positivity) (mem_Icc.1 (dist_mem_Icc_of_Ks_ne_zero hK)).1
@@ -635,7 +649,7 @@ private lemma norm_Ks_sub_Ks_le₀₀ {s : ℤ} {x y y' : X} (hK : Ks s x y ≠
   have : (dist y y' / dist x y) ^ (a : ℝ)⁻¹ ≤ (dist y y' / D ^ s * (4 * D)) ^ (a : ℝ)⁻¹ := by
     apply Real.rpow_le_rpow (div_nonneg dist_nonneg dist_nonneg) this (by positivity)
   rw [Real.mul_rpow (div_nonneg dist_nonneg (Ds0 X s).le) (fourD0 D1).le] at this
-  apply le_trans <| mul_le_mul this (div_vol_le₀ CKa0 hK) (by positivity) (by positivity)
+  apply le_trans <| mul_le_mul this (div_vol_le₀ C_K_pos_real hK) (by simp; positivity) (by positivity)
   rw [(by ring : (dist y y' / D ^ s) ^ (a : ℝ)⁻¹ * (4 * D) ^ (a : ℝ)⁻¹ *
       (2 ^ (2 * a + 100 * a ^ 3) * C_K a / volume.real (ball x (D ^ s))) =
       (4 * D) ^ (a : ℝ)⁻¹ * 2 ^ (2 * a + 100 * a ^ 3) * C_K a / volume.real (ball x (D ^ s)) *
@@ -663,9 +677,8 @@ private lemma norm_Ks_sub_Ks_le₀₁ {s : ℤ} {x y y' : X} (hK : Ks s x y ≠
   rw [this]
   refine mul_le_mul ?_ ψ_ineq (abs_nonneg _) (by positivity)
   apply le_trans <| norm_K_le_vol_inv x y
-  unfold C_K
-  apply le_of_le_of_eq <| div_vol_le₀ (by positivity) hK
-  rw_mod_cast [← pow_add, (show 2 * a + 100 * a ^ 3 + a ^ 3 = 2 * a + 101 * a ^ 3 by ring)]
+  apply le_of_le_of_eq <| div_vol_le₀ C_K_pos_real hK
+  rw_mod_cast [C_K, ← pow_add, (show 2 * a + 100 * a ^ 3 + a ^ 3 = 2 * a + 101 * a ^ 3 by ring)]
 
 -- Special case of `norm_Ks_sub_Ks_le`
 private lemma norm_Ks_sub_Ks_le₀ {s : ℤ} {x y y' : X} (hK : Ks s x y ≠ 0)
@@ -848,8 +861,8 @@ lemma integrable_Ks_x {s : ℤ} {x : X} (hD : 1 < (D : ℝ)) : Integrable (Ks s
       positivity
     · simp only [hy, reduceIte, K₀]
       apply (norm_K_le_vol_inv x y).trans
+      rw [Real.vol]
       gcongr
-      · exact (C_K_pos a).le
       · exact measure_ball_pos_real x _ (div_pos (Ds0 X s) (fourD0 hD))
-      · exact ENNReal.toReal_mono (measure_ball_ne_top x (dist x y)) <|
-          measure_mono <| ball_subset_ball (lt_of_not_ge hy).le
+      · exact measure_ball_ne_top x (dist x y)
+      · exact le_of_not_le hy

Carleson/ToMathlib/Data/ENNReal.lean

@@ -12,6 +12,18 @@ variable {α ι : Type*} {s : Set ι} {t : Finset α}
 
 namespace ENNReal
 
+attribute [simp] ofReal_of_nonpos
+-- protect ENNReal.mul_le_mul_left
+
+theorem ofReal_inv_le {x : ℝ} : ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹ := by
+  obtain hx|hx := lt_or_le 0 x <;> simp [ofReal_inv_of_pos, hx]
+
+theorem ofReal_div_le {x y : ℝ} (hy : 0 ≤ y) :
+    ENNReal.ofReal (x / y) ≤ ENNReal.ofReal x / ENNReal.ofReal y := by
+  simp_rw [div_eq_mul_inv, ofReal_mul' (inv_nonneg.2 hy)]
+  gcongr
+  apply ofReal_inv_le
+
 lemma coe_biSup {f : ι → ℝ≥0} (hf : BddAbove (range f)) :
     ⨆ x ∈ s, f x = ⨆ x ∈ s, (f x : ℝ≥0∞) := by
   simp_rw [bddAbove_def, mem_range, forall_exists_index, forall_apply_eq_imp_iff] at hf

Carleson/TwoSidedCarleson/MainTheorem.lean

@@ -9,11 +9,11 @@ noncomputable section
 /-- The constant used in `two_sided_metric_carleson`.
 Has value `2 ^ (452 * a ^ 3) / (q - 1) ^ 6` in the blueprint. -/
 -- todo: put C_K in NNReal?
-def C10_0_1 (a : ℕ) (q : ℝ≥0) : ℝ≥0 := (⟨C_K a, C_K_pos _ |>.le⟩) ^ 2 * C1_0_2 a q
+def C10_0_1 (a : ℕ) (q : ℝ≥0) : ℝ≥0 := (C_K a) ^ 2 * C1_0_2 a q
 
 lemma C10_0_1_pos {a : ℕ} {q : ℝ≥0} (hq : 1 < q) : 0 < C10_0_1 a q :=
-  _root_.mul_pos (pow_two_pos_of_ne_zero
-    (by simp_rw [ne_eq, ← NNReal.coe_eq_zero, NNReal.coe_mk, C_K_pos _ |>.ne', not_false_eq_true])) (C1_0_2_pos hq)
+  mul_pos (pow_two_pos_of_ne_zero <| by simp_rw [ne_eq, C_K_pos.ne', not_false_eq_true])
+    (C1_0_2_pos hq)
 
 variable {X : Type*} {a : ℕ} [MetricSpace X] [DoublingMeasure X (defaultA a : ℕ)]
 variable {τ C r R : ℝ} {q q' : ℝ≥0}