6. Proof of the Antichain Operator Proposition

This file contains the proofs of Lemma 6.1.4 and Proposition 2.0.3 from the blueprint. Three versions of the latter are provided.

Main results

• dens1_antichain : Lemma 6.1.4.
• antichain_operator: Proposition 2.0.3.

theorem dens1_antichain_rearrange {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {𝔄 : Set (𝔓 X)} {g : X → ℂ} (bg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume) : MeasureTheory.eLpNorm (adjointCarlesonSum 𝔄 g) 2 MeasureTheory.volume ^ 2 ≤ 2 * ∑ p : 𝔓 X with p ∈ 𝔄, ∑ p' : 𝔓 X with p' ∈ 𝔄 ∧ 𝔰 p' ≤ 𝔰 p, ‖∫ (x : X), adjointCarleson p' g x * (starRingEnd ℂ) (adjointCarleson p g x)‖ₑ

noncomputable def dach {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (𝔄 : Set (𝔓 X)) (p : 𝔓 X) (g : X → ℂ) : ENNReal

h(p) in the proof of Lemma 6.1.4 (dens₁ antichain h).

Equations

• One or more equations did not get rendered due to their size.

theorem dens1_antichain_dach {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {𝔄 : Set (𝔓 X)} {g : X → ℂ} (hg : Measurable g) (hgG : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x) : MeasureTheory.eLpNorm (adjointCarlesonSum 𝔄 g) 2 MeasureTheory.volume ^ 2 ≤ ↑(Tile.C6_1_5 a) * 2 ^ (6 * a + 1) * ∑ p : 𝔓 X with p ∈ 𝔄, dach 𝔄 p g * ∫⁻ (y : X) in E p, ‖g y‖ₑ

noncomputable def M14 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (𝔄 : Set (𝔓 X)) (p : ℝ) (g : X → ℂ) : X → ENNReal

The maximalFunction instance that appears in Lemma 6.1.4's proof.

Equations

• M14 𝔄 p g = maximalFunction MeasureTheory.volume 𝔄 𝔠 (fun (x : 𝔓 X) => 14 * ↑(defaultD a) ^ 𝔰 x) p g

theorem eLpNorm_le_M14 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {𝔄 : Set (𝔓 X)} {g : X → ℂ} (hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) {p : 𝔓 X} (mp : p ∈ 𝔄) {x₀ : X} (hx : x₀ ∈ Metric.ball (𝔠 p) (14 * ↑(defaultD a) ^ 𝔰 p)) {r : ℝ} (hr : 0 < r) : MeasureTheory.eLpNorm ((Metric.ball (𝔠 p) (14 * ↑(defaultD a) ^ 𝔰 p)).indicator fun (x : X) => ‖g x‖ₑ) (ENNReal.ofReal r) MeasureTheory.volume ≤ MeasureTheory.volume (Metric.ball (𝔠 p) (14 * ↑(defaultD a) ^ 𝔰 p)) ^ r⁻¹ * M14 𝔄 r g x₀

theorem dach_bound {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {𝔄 : Set (𝔓 X)} {g : X → ℂ} (h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) 𝔄) {p : 𝔓 X} (mp : p ∈ 𝔄) (hg : Measurable g) (hgG : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x) {x₀ : X} (hx : x₀ ∈ Metric.ball (𝔠 p) (14 * ↑(defaultD a) ^ 𝔰 p)) : dach 𝔄 p g ≤ ↑(Antichain.C6_1_6 a) * dens₁ 𝔄 ^ (Antichain.p₆ a)⁻¹ * M14 𝔄 (Antichain.q₆ a) g x₀

Equations (6.1.34) to (6.1.37) in Lemma 6.1.4.

theorem M14_bound {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {𝔄 : Set (𝔓 X)} {g : X → ℂ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : MeasureTheory.eLpNorm (M14 𝔄 (Antichain.q₆ a) g) 2 MeasureTheory.volume ≤ 2 ^ (a + 2) * MeasureTheory.eLpNorm g 2 MeasureTheory.volume

theorem C6_1_4_def (a : ℕ) : C6_1_4 a = 2 ^ ((𝕔 + 5 + 𝕔 / 8) * a ^ 3)

@[irreducible]

def C6_1_4 (a : ℕ) : NNReal

Constant appearing in Lemma 6.1.4. Has value 2 ^ (117 * a ^ 3) in the blueprint.

Equations

• C6_1_4 a = 2 ^ ((𝕔 + 5 + 𝕔 / 8) * a ^ 3)

theorem le_C6_1_4 {a : ℕ} (a4 : 4 ≤ a) : Tile.C6_1_5 a * 2 ^ (6 * a + 1) * Antichain.C6_1_6 a * 2 ^ (a + 2) ≤ C6_1_4 a ^ 2

theorem dens1_antichain_sq {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {𝔄 : Set (𝔓 X)} {g : X → ℂ} (h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) 𝔄) (hg : Measurable g) (hgG : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x) : MeasureTheory.eLpNorm (adjointCarlesonSum 𝔄 g) 2 MeasureTheory.volume ^ 2 ≤ (↑(C6_1_4 a) * dens₁ 𝔄 ^ (8 * ↑a ^ 4)⁻¹ * MeasureTheory.eLpNorm g 2 MeasureTheory.volume) ^ 2

theorem dens1_antichain {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {𝔄 : Set (𝔓 X)} {f g : X → ℂ} (h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) 𝔄) (hf : Measurable f) (hfF : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) (hg : Measurable g) (hgG : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x) : ‖∫ (x : X), (starRingEnd ℂ) (g x) * carlesonSum 𝔄 f x‖ₑ ≤ ↑(C6_1_4 a) * dens₁ 𝔄 ^ (8 * ↑a ^ 4)⁻¹ * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm g 2 MeasureTheory.volume

Lemma 6.1.4.

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

The constant appearing in Proposition 2.0.3. Has value 2 ^ (117 * a ^ 3) in the blueprint.

Equations

• C2_0_3 a q = 2 ^ ((𝕔 + 5 + 𝕔 / 8) * a ^ 3) / (q - 1)

theorem antichain_operator {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {𝔄 : Set (𝔓 X)} {f g : X → ℂ} (h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) 𝔄) (hf : Measurable f) (hf1 : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) (hg : Measurable g) (hg1 : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x) : ‖∫ (x : X), (starRingEnd ℂ) (g x) * carlesonSum 𝔄 f x‖ₑ ≤ ↑(C2_0_3 a (nnq X)) * dens₁ 𝔄 ^ ((q - 1) / (8 * ↑a ^ 4)) * dens₂ 𝔄 ^ (q⁻¹ - 2⁻¹) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm g 2 MeasureTheory.volume

Proposition 2.0.3.

theorem antichain_operator' {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {𝔄 : Set (𝔓 X)} {f : X → ℂ} {A : Set X} (h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) 𝔄) (hf : Measurable f) (hfF : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) (hA : A ⊆ G) : ∫⁻ (x : X) in A, ‖carlesonSum 𝔄 f x‖ₑ ≤ ↑(C2_0_3 a (nnq X)) * dens₁ 𝔄 ^ ((q - 1) / (8 * ↑a ^ 4)) * dens₂ 𝔄 ^ (q⁻¹ - 2⁻¹) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.volume G ^ (1 / 2)

Version of the antichain operator theorem, but controlling the integral of the norm instead of the integral of the function multiplied by another function.

theorem antichain_operator_le_volume {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {𝔄 : Set (𝔓 X)} {f : X → ℂ} {A : Set X} (h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) 𝔄) (hf : Measurable f) (hfF : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) (hA : A ⊆ G) : ∫⁻ (x : X) in A, ‖carlesonSum 𝔄 f x‖ₑ ≤ ↑(C2_0_3 a (nnq X)) * dens₁ 𝔄 ^ ((q - 1) / (8 * ↑a ^ 4)) * dens₂ 𝔄 ^ (q⁻¹ - 2⁻¹) * MeasureTheory.volume F ^ (1 / 2) * MeasureTheory.volume G ^ (1 / 2)

Version of the antichain operator theorem, but controlling the integral of the norm instead of the integral of the function multiplied by another function, and with the upper bound in terms of volume F and volume G.