noncomputable def T_S {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] (Q : MeasureTheory.SimpleFunc X (Θ X)) (s₁ s₂ : ℤ) (f : X → ℂ) (x : X) : ℂ

The operator T_{s₁, s₂} introduced in Lemma 3.0.3.

Equations

• T_S Q s₁ s₂ f x = ∑ s ∈ Finset.Icc s₁ s₂, ∫ (y : X), Ks s x y * f y * Complex.exp (Complex.I * ↑((Q x) y))

theorem measurable_T_inner_integral {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} {f : X → ℂ} {s : ℤ} (mf : Measurable f) : Measurable fun (x : X) => ∫ (y : X), Ks s x y * f y * Complex.exp (Complex.I * ↑((Q x) y))

theorem measurable_T_S {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} {f : X → ℂ} {s₁ s₂ : ℤ} (mf : Measurable f) : Measurable fun (x : X) => T_S Q s₁ s₂ f x

noncomputable def T_lin {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] (Q : MeasureTheory.SimpleFunc X (Θ X)) (σ₁ σ₂ : X → ℤ) (f : X → ℂ) (x : X) : ℂ

The operator T_{2, σ₁, σ₂} introduced in Lemma 3.0.4.

Equations

• T_lin Q σ₁ σ₂ f x = T_S Q (σ₁ x) (σ₂ x) f x

theorem measurable_T_lin {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} {f : X → ℂ} {σ₁ σ₂ : X → ℤ} (mf : Measurable f) (mσ₁ : Measurable σ₁) (mσ₂ : Measurable σ₂) (rσ₁ : (Set.range σ₁).Finite) (rσ₂ : (Set.range σ₂).Finite) : Measurable fun (x : X) => T_lin Q σ₁ σ₂ f x

structure CP304 {X : Type u_1} {a : ℕ} [MetricSpace X] (q q' : NNReal) (F : Set X) {K : X → X → ℂ} [KernelProofData a K] (f : X → ℂ) (σ₁ σ₂ : X → ℤ) : Type u_1

Convenience structure for the parameters that stay constant throughout the recursive calls to finitary Carleson in the proof of Lemma 3.0.4.

• Q : MeasureTheory.SimpleFunc X (Θ X)

  Q is the only non-Prop field of CP304.

• BST_T_Q (θ : Θ X) : MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => linearizedNontangentialOperator (⇑self.Q) θ K x1 x2) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)
• hq : q ∈ Set.Ioc 1 2
• hqq' : q.HolderConjugate q'
• bF : Bornology.IsBounded F
• mF : MeasurableSet F
• mf : Measurable f
• nf : (fun (x : X) => ‖f x‖) ≤ F.indicator 1
• mσ₁ : Measurable σ₁
• mσ₂ : Measurable σ₂
• rσ₁ : (Set.range σ₁).Finite
• rσ₂ : (Set.range σ₂).Finite
• lσ : σ₁ ≤ σ₂

theorem finitary_carleson_step {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [KernelProofData a K] {f : X → ℂ} {σ₁ σ₂ : X → ℤ} [IsCancellative X (defaultτ a)] (CP : CP304 q q' F f σ₁ σ₂) (bG : Bornology.IsBounded G) (mG : MeasurableSet G) : ∃ G' ⊆ G, Bornology.IsBounded G' ∧ MeasurableSet G' ∧ 2 * MeasureTheory.volume G' ≤ MeasureTheory.volume G ∧ ∫⁻ (x : X) in G \ G', ‖T_lin CP.Q σ₁ σ₂ f x‖ₑ ≤ ↑(C2_0_1 a q) * MeasureTheory.volume G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹

structure P304 {X : Type u_1} {a : ℕ} [MetricSpace X] (q q' : NNReal) (F : Set X) {K : X → X → ℂ} [KernelProofData a K] (f : X → ℂ) (σ₁ σ₂ : X → ℤ) : Type u_1

All the parameters needed to apply the recursion of Lemma 3.0.4.

• CP : CP304 q q' F f σ₁ σ₂

  CP holds all constant parameters.

• G : Set X

  G is the set being recursed on.

• bG : Bornology.IsBounded self.G
• mG : MeasurableSet self.G

def P304.succ {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F : Set X} {K : X → X → ℂ} [KernelProofData a K] {f : X → ℂ} {σ₁ σ₂ : X → ℤ} [IsCancellative X (defaultτ a)] (P : P304 q q' F f σ₁ σ₂) : P304 q q' F f σ₁ σ₂

Construct G_{n+1} given G_n.

Equations

• P.succ = { CP := P.CP, G := ⋯.choose, bG := ⋯, mG := ⋯ }

def slice {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [KernelProofData a K] {f : X → ℂ} {σ₁ σ₂ : X → ℤ} [IsCancellative X (defaultτ a)] (CP : CP304 q q' F f σ₁ σ₂) (bG : Bornology.IsBounded G) (mG : MeasurableSet G) (n : ℕ) : P304 q q' F f σ₁ σ₂

slice CP bG mG n contains G_n and its associated data.

Equations

• slice CP bG mG n = P304.succ^[n] { CP := CP, G := G, bG := bG, mG := mG }

@[simp]

theorem slice_CP {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [KernelProofData a K] {f : X → ℂ} {σ₁ σ₂ : X → ℤ} [IsCancellative X (defaultτ a)] {CP : CP304 q q' F f σ₁ σ₂} {bG : Bornology.IsBounded G} {mG : MeasurableSet G} {n : ℕ} : (slice CP bG mG n).CP = CP

theorem slice_G_subset {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [KernelProofData a K] {f : X → ℂ} {σ₁ σ₂ : X → ℤ} [IsCancellative X (defaultτ a)] {CP : CP304 q q' F f σ₁ σ₂} {bG : Bornology.IsBounded G} {mG : MeasurableSet G} {n : ℕ} : (slice CP bG mG (n + 1)).G ⊆ (slice CP bG mG n).G

theorem antitone_slice_G {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [KernelProofData a K] {f : X → ℂ} {σ₁ σ₂ : X → ℤ} [IsCancellative X (defaultτ a)] {CP : CP304 q q' F f σ₁ σ₂} {bG : Bornology.IsBounded G} {mG : MeasurableSet G} : Antitone fun (n : ℕ) => (slice CP bG mG n).G

theorem volume_slice {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [KernelProofData a K] {f : X → ℂ} {σ₁ σ₂ : X → ℤ} [IsCancellative X (defaultτ a)] {CP : CP304 q q' F f σ₁ σ₂} {bG : Bornology.IsBounded G} {mG : MeasurableSet G} {n : ℕ} : 2 * MeasureTheory.volume (slice CP bG mG (n + 1)).G ≤ MeasureTheory.volume (slice CP bG mG n).G

theorem volume_slice_le_inv_two_pow_mul {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [KernelProofData a K] {f : X → ℂ} {σ₁ σ₂ : X → ℤ} [IsCancellative X (defaultτ a)] {CP : CP304 q q' F f σ₁ σ₂} {bG : Bornology.IsBounded G} {mG : MeasurableSet G} {n : ℕ} : MeasureTheory.volume (slice CP bG mG n).G ≤ 2⁻¹ ^ n * MeasureTheory.volume G

theorem exists_volume_slice_lt_eps {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [KernelProofData a K] {f : X → ℂ} {σ₁ σ₂ : X → ℤ} [IsCancellative X (defaultτ a)] {CP : CP304 q q' F f σ₁ σ₂} {bG : Bornology.IsBounded G} {mG : MeasurableSet G} {ε : ENNReal} (εpos : 0 < ε) : ∃ (n : ℕ), MeasureTheory.volume (slice CP bG mG (n + 1)).G < ε

The sets G_n become arbitrarily small.

theorem slice_integral_bound {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [KernelProofData a K] {f : X → ℂ} {σ₁ σ₂ : X → ℤ} [IsCancellative X (defaultτ a)] {CP : CP304 q q' F f σ₁ σ₂} {bG : Bornology.IsBounded G} {mG : MeasurableSet G} {n : ℕ} : ∫⁻ (x : X) in (slice CP bG mG n).G \ (slice CP bG mG (n + 1)).G, ‖T_lin CP.Q σ₁ σ₂ f x‖ₑ ≤ ↑(C2_0_1 a q) * MeasureTheory.volume (slice CP bG mG n).G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹

theorem slice_integral_bound_sum {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [KernelProofData a K] {f : X → ℂ} {σ₁ σ₂ : X → ℤ} [IsCancellative X (defaultτ a)] {CP : CP304 q q' F f σ₁ σ₂} {bG : Bornology.IsBounded G} {mG : MeasurableSet G} {n : ℕ} : ∫⁻ (x : X), (G \ (slice CP bG mG (n + 1)).G).indicator (fun (x : X) => ‖T_lin CP.Q σ₁ σ₂ f x‖ₑ) x ≤ (↑(C2_0_1 a q) * ∑ i ∈ Finset.range (n + 1), (2⁻¹ ^ i) ^ (↑q')⁻¹) * MeasureTheory.volume G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹

The slightly unusual way of writing the integrand is to facilitate applying the monotone convergence theorem.

theorem sum_le_four_div_q_sub_one {q q' : NNReal} (hq : q ∈ Set.Ioc 1 2) (hqq' : q.HolderConjugate q') {n : ℕ} : ∑ i ∈ Finset.range n, (2⁻¹ ^ i) ^ (↑q')⁻¹ ≤ ↑(2 ^ 2 / (q - 1))

noncomputable def C3_0_4 (a : ℕ) (q : NNReal) : NNReal

The constant used in linearized_truncation and S_truncation. Has value 2 ^ (442 * a ^ 3 + 2) in the blueprint.

Equations

• C3_0_4 a q = 2 ^ ((3 * 𝕔 + 17 + 5 * (𝕔 / 4)) * a ^ 3 + 2) / (q - 1) ^ 6

theorem eq_C3_0_4 {a : ℕ} {q : NNReal} : C2_0_1 a q * (2 ^ 2 / (q - 1)) = C3_0_4 a q

theorem linearized_truncation {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} {f : X → ℂ} {σ₁ σ₂ : X → ℤ} [IsCancellative X (defaultτ a)] (hq : q ∈ Set.Ioc 1 2) (hqq' : q.HolderConjugate q') (bF : Bornology.IsBounded F) (bG : Bornology.IsBounded G) (mF : MeasurableSet F) (mG : MeasurableSet G) (mf : Measurable f) (nf : (fun (x : X) => ‖f x‖) ≤ F.indicator 1) (mσ₁ : Measurable σ₁) (mσ₂ : Measurable σ₂) (rσ₁ : (Set.range σ₁).Finite) (rσ₂ : (Set.range σ₂).Finite) (lσ : σ₁ ≤ σ₂) (BST_T_Q : ∀ (θ : Θ X), MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => linearizedNontangentialOperator (⇑Q) θ K x1 x2) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) : ∫⁻ (x : X) in G, ‖T_lin Q σ₁ σ₂ f x‖ₑ ≤ ↑(C3_0_4 a q) * MeasureTheory.volume G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹

Lemma 3.0.4.

theorem S_truncation {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} {f : X → ℂ} [IsCancellative X (defaultτ a)] {B : ℕ} (hq : q ∈ Set.Ioc 1 2) (hqq' : q.HolderConjugate q') (bF : Bornology.IsBounded F) (bG : Bornology.IsBounded G) (mF : MeasurableSet F) (mG : MeasurableSet G) (mf : Measurable f) (nf : (fun (x : X) => ‖f x‖) ≤ F.indicator 1) (BST_T_Q : ∀ (θ : Θ X), MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => linearizedNontangentialOperator (⇑Q) θ K x1 x2) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) : ∫⁻ (x : X) in G, ⨆ s₁ ∈ Finset.Icc (-↑B) ↑B, ⨆ s₂ ∈ Finset.Icc s₁ ↑B, ‖T_S Q s₁ s₂ f x‖ₑ ≤ ↑(C3_0_4 a q) * MeasureTheory.volume G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹

Lemma 3.0.3. B is the blueprint's S.

noncomputable def L302 (a : ℕ) (R₁ : ℝ) : ℤ

The largest integer s₁ satisfying D ^ (-(s₁ - 2)) * R₁ > 1 / 2.

Equations

• L302 a R₁ = ⌊Real.logb (↑(defaultD a)) (2 * R₁)⌋ + 3

noncomputable def U302 (a : ℕ) (R₂ : ℝ) : ℤ

The smallest integer s₂ satisfying D ^ (-(s₂ + 2)) * R₂ < 1 / (4 * D).

Equations

• U302 a R₂ = ⌈Real.logb (↑(defaultD a)) (4 * R₂)⌉ - 2

theorem R₁_le_D_zpow_div_four {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] {R₁ : ℝ} : R₁ ≤ ↑(defaultD a) ^ (L302 a R₁ - 1) / 4

theorem D_zpow_div_two_le_R₂ {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] {R₂ : ℝ} (hR₂ : 0 < R₂) : ↑(defaultD a) ^ U302 a R₂ / 2 ≤ R₂

theorem monotoneOn_L302 {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] : MonotoneOn (L302 a) {r : ℝ | 0 < r}

theorem monotoneOn_U302 {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] : MonotoneOn (U302 a) {r : ℝ | 0 < r}

theorem exists_uniform_annulus_bound {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] {R : ℝ} (hR : 0 < R) : ∃ (B : ℕ), ∀ R₁ ∈ Set.Ioo R⁻¹ R, ∀ R₂ ∈ Set.Ioo R₁ R, L302 a R₁ ∈ Finset.Icc (-↑B) ↑B ∧ U302 a R₂ ∈ Finset.Icc (-↑B) ↑B

There exists a uniform bound for all possible values of L302 and U302 over the annulus in R_truncation.

theorem enorm_setIntegral_annulus_le {X : Type u_1} {a : ℕ} [MetricSpace X] {F : Set X} {K : X → X → ℂ} [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} {f : X → ℂ} {x : X} {R₁ R₂ : ℝ} {s : ℤ} (nf : (fun (x : X) => ‖f x‖) ≤ F.indicator 1) : ‖∫ (y : X) in Set.Annulus.oo x R₁ R₂, Ks s x y * f y * Complex.exp (Complex.I * ↑((Q x) y))‖ₑ ≤ ↑(C2_1_3 a) * globalMaximalFunction MeasureTheory.volume 1 (F.indicator 1) x

noncomputable def edgeScales (a : ℕ) (R₁ R₂ : ℝ) : Finset ℤ

The fringes of the scale interval in Lemma 3.0.2's proof that require separate handling.

Equations

• edgeScales a R₁ R₂ = {L302 a R₁ - 1, L302 a R₁ - 2, U302 a R₂ + 1, U302 a R₂ + 2}

theorem diff_subset_edgeScales {a : ℕ} {R₁ R₂ : ℝ} : Finset.Icc (L302 a R₁ - 2) (U302 a R₂ + 2) \ Finset.Icc (L302 a R₁) (U302 a R₂) ⊆ edgeScales a R₁ R₂

theorem enorm_carlesonOperatorIntegrand_le_T_S {X : Type u_1} {a : ℕ} [MetricSpace X] {F : Set X} {K : X → X → ℂ} [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} {f : X → ℂ} {R₁ R₂ : ℝ} (hR₁ : 0 < R₁) (hR₂ : R₁ < R₂) (mf : Measurable f) (nf : (fun (x : X) => ‖f x‖) ≤ F.indicator 1) {x : X} : ‖carlesonOperatorIntegrand K (Q x) R₁ R₂ f x‖ₑ ≤ ‖T_S Q (L302 a R₁) (U302 a R₂) f x‖ₑ + 4 * ↑(C2_1_3 a) * globalMaximalFunction MeasureTheory.volume 1 (F.indicator 1) x

theorem lintegral_globalMaximalFunction_le {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [KernelProofData a K] (hq : q ∈ Set.Ioc 1 2) (hqq' : q.HolderConjugate q') (bF : Bornology.IsBounded F) (mF : MeasurableSet F) (mG : MeasurableSet G) : ∫⁻ (x : X) in G, globalMaximalFunction MeasureTheory.volume 1 (F.indicator 1) x ≤ ↑(C2_0_6 (↑(defaultA a)) 1 q) * MeasureTheory.volume G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹

noncomputable def T_R {X : Type u_1} {a : ℕ} [MetricSpace X] {K : X → X → ℂ} [KernelProofData a K] : (X → X → ℂ) → (Q : MeasureTheory.SimpleFunc X (Θ X)) → (R₁ R₂ R : ℝ) → (f : X → ℂ) → (x : X) → ℂ

The operator T_{R₁, R₂, R} introduced in Lemma 3.0.2.

Equations

• T_R K Q R₁ R₂ R f x = (Metric.ball (cancelPt X) R).indicator (fun (x : X) => carlesonOperatorIntegrand K (Q x) R₁ R₂ f x) x

theorem C1_0_2_pos {a : ℕ} {q : NNReal} (hq : 1 < q) : 0 < C1_0_2 a q

theorem le_C1_0_2 {a : ℕ} {q : NNReal} (a4 : 4 ≤ a) (hq : q ∈ Set.Ioc 1 2) : C3_0_4 a q + 4 * C2_1_3 a * C2_0_6 (↑(defaultA a)) 1 q ≤ C1_0_2 a q

theorem R_truncation' {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} {f : X → ℂ} [IsCancellative X (defaultτ a)] (hq : q ∈ Set.Ioc 1 2) (hqq' : q.HolderConjugate q') (mF : MeasurableSet F) (mG : MeasurableSet G) (mf : Measurable f) (nf : (fun (x : X) => ‖f x‖) ≤ F.indicator 1) {n : ℕ} {R : ℝ} (hR : R = 2 ^ n) (sF : F ⊆ Metric.ball (cancelPt X) (2 * R)) (sG : G ⊆ Metric.ball (cancelPt X) R) (BST_T_Q : ∀ (θ : Θ X), MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => linearizedNontangentialOperator (⇑Q) θ K x1 x2) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) : ∫⁻ (x : X) in G, ⨆ R₁ ∈ Set.Ioo R⁻¹ R, ⨆ R₂ ∈ Set.Ioo R₁ R, ‖T_R K Q R₁ R₂ R f x‖ₑ ≤ ↑(C1_0_2 a q) * MeasureTheory.volume G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹

theorem R_truncation {X : Type u_1} {a : ℕ} [MetricSpace X] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} {f : X → ℂ} [IsCancellative X (defaultτ a)] (hq : q ∈ Set.Ioc 1 2) (hqq' : q.HolderConjugate q') (mF : MeasurableSet F) (mG : MeasurableSet G) (mf : Measurable f) (nf : (fun (x : X) => ‖f x‖) ≤ F.indicator 1) {n : ℕ} {R : ℝ} (hR : R = 2 ^ n) (BST_T_Q : ∀ (θ : Θ X), MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => linearizedNontangentialOperator (⇑Q) θ K x1 x2) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) : ∫⁻ (x : X) in G, ⨆ R₁ ∈ Set.Ioo R⁻¹ R, ⨆ R₂ ∈ Set.Ioo R₁ R, ‖T_R K Q R₁ R₂ R f x‖ₑ ≤ ↑(C1_0_2 a q) * MeasureTheory.volume G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹

Lemma 3.0.2.