Proof of Lemma 10.0.1 (#451)

A bit ugly, but it works

Author: js2357

Carleson/Defs.lean

@@ -292,6 +292,28 @@ Use `ENNReal.toReal` to get the corresponding real number. -/
 def carlesonOperator [FunctionDistances ℝ X] (K : X → X → ℂ) (f : X → ℂ) (x : X) : ℝ≥0∞ :=
   ⨆ (θ : Θ X), linearizedCarlesonOperator (fun _ ↦ θ) K f x
 
+private lemma carlesonOperatorIntegrand_const_smul [FunctionDistances ℝ X] (K : X → X → ℂ)
+    (θ : Θ X) (R₁ R₂ : ℝ) (f : X → ℂ) (z : ℂ) :
+    carlesonOperatorIntegrand (z • K) θ R₁ R₂ f = z • carlesonOperatorIntegrand K θ R₁ R₂ f := by
+  unfold carlesonOperatorIntegrand
+  ext x
+  simp_rw [Pi.smul_apply, smul_eq_mul, ← integral_const_mul]
+  congr with y
+  ring
+
+private lemma linearizedCarlesonOperator_const_smul [FunctionDistances ℝ X] (Q : X → Θ X)
+    (K : X → X → ℂ) (f : X → ℂ) (z : ℂ) :
+    linearizedCarlesonOperator Q (z • K) f = ‖z‖ₑ • linearizedCarlesonOperator Q K f := by
+  unfold linearizedCarlesonOperator
+  simp_rw [carlesonOperatorIntegrand_const_smul, Pi.smul_apply, smul_eq_mul, enorm_mul, ← mul_iSup]
+  rfl
+
+lemma carlesonOperator_const_smul [FunctionDistances ℝ X] (K : X → X → ℂ) (f : X → ℂ) (z : ℂ) :
+    carlesonOperator (z • K) f = ‖z‖ₑ • carlesonOperator K f := by
+  unfold carlesonOperator
+  simp_rw [linearizedCarlesonOperator_const_smul, Pi.smul_apply, ← smul_iSup]
+  rfl
+
 end DoublingMeasure
 
 /-- This is usually the value of the argument `A` in `DoublingMeasure`
@@ -340,6 +362,19 @@ class IsOneSidedKernel (a : outParam ℕ) (K : X → X → ℂ) : Prop where
 
 export IsOneSidedKernel (measurable_K norm_K_le_vol_inv norm_K_sub_le)
 
+lemma isOneSidedKernel_const_smul {a : ℕ} {K : X → X → ℂ} [IsOneSidedKernel a K] {r : ℝ}
+    (hr : |r| ≤ 1) :
+    IsOneSidedKernel a (r • K) where
+  measurable_K := measurable_K.const_smul r
+  norm_K_le_vol_inv x y := by
+    convert mul_le_mul hr (norm_K_le_vol_inv (K := K) x y) (norm_nonneg _) (zero_le_one' ℝ) using 1
+    all_goals simp
+  norm_K_sub_le h := by
+    simp only [Pi.smul_apply, real_smul]
+    rw [← one_mul (_ ^ _ * _), ← mul_sub, Complex.norm_mul, norm_real, Real.norm_eq_abs]
+    gcongr
+    exact norm_K_sub_le h
+
 lemma MeasureTheory.stronglyMeasurable_K [IsOneSidedKernel a K] :
     StronglyMeasurable (uncurry K) :=
   measurable_K.stronglyMeasurable
@@ -418,7 +453,7 @@ lemma integrableOn_K_Icc [IsOpenPosMeasure (volume : Measure X)]
     IntegrableOn (K x) {y | dist x y ∈ Icc r R} volume := by
   rw [← mul_one (K x)]
   refine integrableOn_K_mul ?_ x hr ?_
-  · have : {y | dist x y ∈ Icc r R} ⊆ closedBall x R := by intro y; simp [dist_comm y x]
+  · have : {y | dist x y ∈ Icc r R} ⊆ closedBall x R := Annulus.cc_subset_closedBall
     exact integrableOn_const ((measure_mono this).trans_lt measure_closedBall_lt_top).ne
   · intro y hy; simp [hy.1, dist_comm y x]
 

Carleson/ToMathlib/WeakType.lean

@@ -523,6 +523,13 @@ lemma HasBoundedStrongType.hasBoundedWeakType (hp' : 0 < p')
   fun f hf ↦
     ⟨(h f hf).1, wnorm_le_eLpNorm (h f hf).1 hp' |>.trans (h f hf).2⟩
 
+lemma HasBoundedStrongType.const_smul {T : (α → ε₁) → α' → ℝ≥0∞}
+    (h : HasBoundedStrongType T p p' μ ν c) (r : ℝ≥0) :
+    HasBoundedStrongType (r • T) p p' μ ν (r • c) := by
+  intro f hf
+  rw [Pi.smul_apply, MeasureTheory.eLpNorm_const_smul']
+  exact ⟨(h f hf).1.const_smul _, le_of_le_of_eq (mul_le_mul_left' (h f hf).2 ‖r‖ₑ) (by simp; rfl)⟩
+
 end HasBoundedStrongType
 
 section distribution

Carleson/TwoSidedCarleson/MainTheorem.lean

@@ -30,7 +30,32 @@ theorem two_sided_metric_carleson (ha : 4 ≤ a) (hq : q ∈ Ioc 1 2) (hqq' : q.
     {f : X → ℂ} (hmf : Measurable f) (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
     ∫⁻ x in G, carlesonOperator K f x ≤
     C10_0_1 a q * (volume G) ^ (q' : ℝ)⁻¹ * (volume F) ^ (q : ℝ)⁻¹ := by
-  -- note: you might need to case on whether `volume F` is `∞` or not.
-  sorry
+  let c := (2 : ℝ) ^ (-2 * (a : ℝ) ^ 3)
+  have c_pos : 0 < c := Real.rpow_pos_of_pos two_pos _
+  have : IsOneSidedKernel a (c • K) := by
+    apply isOneSidedKernel_const_smul
+    unfold c
+    rw [neg_mul, Real.abs_rpow_of_nonneg two_pos.le, abs_two]
+    exact Real.rpow_le_one_of_one_le_of_nonpos one_le_two (by norm_num)
+  let : KernelProofData a (c • K) := by constructor <;> assumption
+  have : nontangentialOperator (c • K) = ‖c‖ₑ • nontangentialOperator K := by
+    convert nontangentialOperator_const_smul (c : ℂ)
+    rw [← ofReal_norm_eq_enorm, ← ofReal_norm_eq_enorm, Complex.norm_real]
+  have HBST : HasBoundedStrongType (nontangentialOperator (c • K)) 2 2 volume volume (C_Ts a) := by
+    rw [this, ← ofReal_norm_eq_enorm]
+    convert HasBoundedStrongType.const_smul (nontangential_from_simple ha hT) ‖c‖.toNNReal
+    rw [C_Ts, C10_0_2_def, coe_pow, coe_ofNat, ← rpow_natCast, Nat.cast_pow, ENNReal.smul_def,
+      Real.norm_eq_abs, ofNNReal_toNNReal, abs_of_pos c_pos, ← ofReal_rpow_of_pos two_pos,
+      coe_pow, coe_ofNat, ← rpow_natCast, Nat.cast_mul, Nat.cast_ofNat, Nat.cast_pow,
+      ofReal_ofNat 2, smul_eq_mul, ← rpow_add _ _ (NeZero.ne 2) ENNReal.ofNat_ne_top]
+    ring_nf
+  rw [← ENNReal.mul_le_mul_left (enorm_ne_zero.mpr c_pos.ne') enorm_ne_top,
+    ← lintegral_const_mul' _ _ enorm_ne_top, mul_assoc, ← mul_assoc, ← mul_assoc]
+  convert metric_carleson hq hqq' hF hG hmf hf HBST
+  · convert congrFun (carlesonOperator_const_smul K f (c : ℂ)) _ |>.symm; simp
+  rw [C10_0_1, C_K, coe_mul, ← mul_assoc, ← ofReal_coe_nnreal, Real.enorm_eq_ofReal c_pos.le,
+    ← ofReal_mul c_pos.le, NNReal.coe_pow, NNReal.coe_rpow, NNReal.coe_ofNat,
+    ← Real.rpow_mul_natCast two_pos.le, ← Real.rpow_add two_pos,
+    ofReal_eq_one.mpr (by ring_nf; exact Real.rpow_zero 2), one_mul]
 
 end

Carleson/TwoSidedCarleson/NontangentialOperator.lean

@@ -1173,4 +1173,11 @@ theorem nontangential_from_simple (ha : 4 ≤ a)
       _ ≤ a ^ 3 + 2 * a * a * a := by gcongr
       _ = _ := by ring
 
+omit [IsTwoSidedKernel a K] in
+lemma nontangentialOperator_const_smul (z : ℂ) :
+    nontangentialOperator (z • K) = ‖z‖ₑ • nontangentialOperator K := by
+  unfold nontangentialOperator
+  simp_rw [Pi.smul_apply, smul_eq_mul, mul_assoc, integral_const_mul, enorm_mul, ← ENNReal.mul_iSup]
+  rfl
+
 end

blueprint/src/chapter/main.tex

@@ -6896,6 +6896,7 @@ \chapter{Two-sided Metric Space Carleson}
 
 \begin{proof}[Proof of \Cref{two-sided-metric-space-Carleson}]
     \proves{two-sided-metric-space-Carleson}
+    \leanok
     Let $1<q\le 2$ be a real number. Let $\Theta$ be a cancellative compatible collection of functions.
     By the assumption \eqref{two-sided-Hr-bound-assumption}, we can apply \Cref{nontangential-from-simple} to obtain for every bounded measurable $g:X\to\C$ supported on a set of finite measure,
     \begin{equation}\label{original-operator-assumption}