Add lemma statements from section 6.2

Carleson.lean

@@ -1,5 +1,6 @@
 import Carleson.Antichain.AntichainOperator
 import Carleson.Antichain.AntichainTileCount
+import Carleson.Antichain.TileCorrelation
 import Carleson.Classical.Approximation
 import Carleson.Classical.Basic
 import Carleson.Classical.CarlesonOnTheRealLine

Carleson/Antichain/AntichainOperator.lean

@@ -300,7 +300,7 @@ lemma _root_.Set.eq_indicator_one_mul {F : Set X} {f : X → ℂ} (hf : ∀ x, 
 /-- Constant appearing in Lemma 6.1.3. -/
 noncomputable def C_6_1_3 (a : ℝ) (q : ℝ≥0) : ℝ≥0 := 2^(111*a^3)*(q-1)⁻¹
 
--- Inequality 6.1.15
+-- Inequality 6.1.16
 lemma eLpNorm_maximal_function_le' {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤·) (𝔄 : Set (𝔓 X)))
     {f : X → ℂ} (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (hfm : Measurable f) :
     eLpNorm (fun x ↦ (maximalFunction volume (↑𝔄) 𝔠 (fun 𝔭 ↦ 8 * ↑D ^ 𝔰 𝔭)
@@ -510,8 +510,8 @@ def C_2_0_3 (a q : ℝ) : ℝ := 2 ^ (150 * a ^ 3) / (q - 1)
 
 /-- Proposition 2.0.3 -/
 theorem antichain_operator {𝔄 : Set (𝔓 X)} {f g : X → ℂ}
-    (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x)
-    (hg : Measurable g) (hg : ∀ x, ‖g x‖ ≤ G.indicator 1 x)
+    (hf : Measurable f) (hf1 : ∀ x, ‖f x‖ ≤ F.indicator 1 x)
+    (hg : Measurable g) (hg1 : ∀ x, ‖g x‖ ≤ G.indicator 1 x)
     (h𝔄 : IsAntichain (·≤·) (toTileLike (X := X) '' 𝔄)) :
     ‖∫ x, conj (g x) * ∑ᶠ p : 𝔄, carlesonOn p f x‖ ≤
     C_2_0_3 a q * (dens₁ 𝔄).toReal ^ ((q - 1) / (8 * a ^ 4)) * (dens₂ 𝔄).toReal ^ (q⁻¹ - 2⁻¹) *

Carleson/Antichain/TileCorrelation.lean

@@ -0,0 +1,81 @@
+import Carleson.ForestOperator.AlmostOrthogonality
+import Carleson.HardyLittlewood
+import Carleson.Psi
+import Carleson.TileStructure
+
+
+noncomputable section
+
+open scoped ComplexConjugate ENNReal NNReal ShortVariables
+
+open MeasureTheory Metric Set
+
+namespace Tile
+
+variable {X : Type*} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X]
+  [ProofData a q K σ₁ σ₂ F G]
+
+-- Def 6.2.1 (Lemma 6.2.1)
+def correlation (s₁ s₂ : ℤ) (x₁ x₂ y : X) : ℂ := (conj (Ks s₁ x₁ y)) * (Ks s₂ x₂ y)
+
+-- Eq. 6.2.2 (Lemma 6.2.1)
+lemma mem_ball_of_correlation_ne_zero {s₁ s₂ : ℤ} {x₁ x₂ y : X}
+    (hy : correlation s₁ s₂ x₁ x₂ y ≠ 0) : y ∈ (ball x₁ (↑D ^s₁)) := by
+  have hKs : Ks s₁ x₁ y ≠ 0 := by
+    simp only [correlation, ne_eq, mul_eq_zero, map_eq_zero, not_or] at hy
+    exact hy.1
+  rw [mem_ball, dist_comm]
+  exact lt_of_le_of_lt (dist_mem_Icc_of_Ks_ne_zero hKs).2
+    (half_lt_self_iff.mpr (defaultD_pow_pos a s₁))
+
+def C_6_2_1 (a : ℕ) : ℝ≥0 := 2^(254 * a^3)
+
+-- Eq. 6.2.3 (Lemma 6.2.1)
+lemma correlation_kernel_bound {s₁ s₂ : ℤ} (hs₁ : s₁ ∈ Icc (- (S : ℤ)) s₂)
+    (hs₂ : s₂ ∈ Icc s₁ S) {x₁ x₂ y : X} (hy : correlation s₁ s₂ x₁ x₂ y ≠ 0)/- Is hy needed?-/ :
+    hnorm (a := a) (correlation s₁ s₂ x₁ x₂) x₁ ↑D ^s₁ ≤
+    (C_6_2_1 a : ℝ≥0∞) / (volume (ball x₁ (↑D ^s₁)) * volume (ball x₂ (↑D ^s₂))) := by
+  sorry
+
+variable [TileStructure Q D κ S o]
+
+def C_6_2_2 (a : ℕ) : ℝ≥0 := 2^(3 * a)
+
+-- Lemma 6.2.2
+lemma uncertainty {p₁ p₂ : 𝔓 X} (hle : 𝔰 p₁ ≤ 𝔰 p₂) {x₁ x₂ : X} (hx₁ : x₁ ∈ E p₁)
+    (hx₂ : x₂ ∈ E p₂) :
+    1  + dist_(p₁) (𝒬 p₁) (𝒬 p₂) ≤ (C_6_2_2 a) * (1 + dist_{x₁, D^𝔰 p₁} (Q x₁) (Q x₂)) :=
+  sorry
+
+open TileStructure.Forest
+
+-- Lemma 6.2.3
+lemma range_support {p : 𝔓 X} {g : X → ℂ} (hg : Measurable g)
+    (hg1 : ∀ x, ‖g x‖ ≤ G.indicator 1 x) {y : X} (hpy : adjointCarleson p g y ≠ 0) :
+    y ∈ (ball (𝔠 p) (5 * ↑D ^𝔰 p)) :=
+  sorry
+
+def C_6_1_5 (a : ℕ) : ℝ≥0 := 2^(255 * a^3)
+
+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
+  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
+  by_contra h0
+  apply hpp'
+  have hy : ∃ y : X, (adjointCarleson p' g y) * conj (adjointCarleson p g y) ≠ 0 := sorry
+  obtain ⟨y, hy⟩ := hy
+  sorry
+
+end Tile

blueprint/src/chapter/main.tex

@@ -3542,6 +3542,8 @@ \section{The density arguments}\label{sec-TT*-T*T}
 The following basic $TT^*$ estimate will be proved in \Cref{sec-tile-operator}.
 \begin{lemma}[tile correlation]
     \label{tile-correlation}
+    \leanok
+    \lean{Tile.correlation_le, Tile.correlation_zero_of_ne_subset}
     \uses{Holder-van-der-Corput,correlation-kernel-bound,tile-uncertainty,tile-range-support}
     Let $\fp, \fp'\in \fP$ with
     $\ps({\fp'})\leq \ps({\fp})$.
@@ -3602,6 +3604,8 @@ \section{Proof of the Tile Correlation Lemma}\label{sec-tile-operator}
 The next lemma prepares an application of
 \Cref{Holder-van-der-Corput}.
 \begin{lemma}[correlation kernel bound]\label{correlation-kernel-bound}
+\leanok
+\lean{Tile.correlation, Tile.mem_ball_of_correlation_ne_zero, Tile.correlation_kernel_bound}
 Let $-S\le s_1\le s_2\le S$ and let $x_1,x_2\in X$.
 Define \begin{equation}
  \varphi(y) := \overline{K_{s_1}(x_1, y)}
@@ -3655,6 +3659,8 @@ \section{Proof of the Tile Correlation Lemma}\label{sec-tile-operator}
 \end{proof}
 The next lemma is a geometric estimate for two tiles.
 \begin{lemma}\label{tile-uncertainty}
+\leanok
+\lean{Tile.uncertainty}
 \uses{monotone-cube-metrics}
     Let $\fp_1, \fp_2\in \fP$ with
 $\ps({\fp_1})\leq \ps({\fp_2})$. For each $x_1\in E(\fp_1)$ and
@@ -3704,6 +3710,8 @@ \section{Proof of the Tile Correlation Lemma}\label{sec-tile-operator}
 
 
 \begin{lemma}[tile range support]\label{tile-range-support}
+\leanok
+\lean{Tile.range_support}
     For each $\fp\in \fP$, and each $y\in X$, we have that
 \begin{equation}\label{tstargnot0}
      T_{\fp}^* g(y)\neq 0