theorem E_disjoint {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) ↑𝔄) {p : 𝔓 X} {p' : 𝔓 X} (hp : p ∈ 𝔄) (hp' : p' ∈ 𝔄) (hE : (E p ∩ E p').Nonempty) : p = p'

noncomputable def C_6_1_2 (a : ℕ) : ℕ

Constant appearing in Lemma 6.1.2.

Equations

• C_6_1_2 a = 2 ^ (107 * a ^ 3)

theorem C_6_1_2_ne_zero (a : ℕ) : ↑(C_6_1_2 a) ≠ 0

theorem ENNReal.div_mul (a : ENNReal) {b : ENNReal} {c : ENNReal} (hb0 : b ≠ 0) (hb_top : b ≠ ⊤) (hc0 : c ≠ 0) (hc_top : c ≠ ⊤) : a / b * c = a / (b / c)

theorem norm_Ks_le' {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {x : X} {y : X} {𝔄 : Set (𝔓 X)} (p : ↑𝔄) (hy : Ks (𝔰 ↑p) x y ≠ 0) : ‖Ks (𝔰 ↑p) x y‖₊ ≤ 2 ^ (5 * a + 101 * a ^ 3) / MeasureTheory.volume.nnreal (Metric.ball x (8 * ↑(defaultD a) ^ 𝔰 ↑p))

theorem MaximalBoundAntichain {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F✝ G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) ↑𝔄) (ha : 1 ≤ a) {F : Set X} {f : X → ℂ} (hf : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) (x : X) : ↑‖∑ p ∈ 𝔄, carlesonOn p f x‖₊ ≤ ↑(C_6_1_2 a) * MB MeasureTheory.volume (↑𝔄) 𝔠 (fun (𝔭 : 𝔓 X) => 8 * ↑(defaultD a) ^ 𝔰 𝔭) f x

noncomputable def C_6_1_3 (a : ℝ) (q : NNReal) : NNReal

Constant appearing in Lemma 6.1.3.

Equations

• C_6_1_3 a q = 2 ^ (111 * a ^ 3) * (q - 1)⁻¹

def ShortVariables.termQ' : Lean.ParserDescr

Equations

• ShortVariables.termQ' = Lean.ParserDescr.node `ShortVariables.termQ' 1024 (Lean.ParserDescr.symbol "q'")

theorem Dens2Antichain {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) ↑𝔄) (ha : 4 ≤ a) {f : X → ℂ} (hf : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) {g : X → ℂ} (hg : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x) (x : X) : ↑‖∫ (x : X), (starRingEnd ℂ) (g x) * ∑ p ∈ 𝔄, carlesonOn p f x‖₊ ≤ ↑(C_6_1_3 (↑a) (nnq X)) * dens₂ ↑𝔄 ^ ((2 * ↑(nnq X) / (↑(nnq X) + 1))⁻¹ - 2⁻¹) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm g 2 MeasureTheory.volume

def C_2_0_3 (a : ℝ) (q : ℝ) : ℝ

The constant appearing in Proposition 2.0.3. Has value 2 ^ (150 * a ^ 3) / (q - 1) in the blueprint.

Equations

• C_2_0_3 a q = 2 ^ (150 * a ^ 3) / (q - 1)

theorem antichain_operator {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {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 → ℂ} {g : X → ℂ} (hf : Measurable f) (h2f : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) (hg : Measurable g) (hg : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x) (h𝔄 : IsAntichain (fun (x1 x2 : TileLike X) => x1 ≤ x2) (toTileLike '' 𝔄)) : ‖∫ (x : X), (starRingEnd ℂ) (g x) * ∑ᶠ (p : ↑𝔄), carlesonOn (↑p) f x‖ ≤ C_2_0_3 (↑a) q * (dens₁ 𝔄).toReal ^ ((q - 1) / (8 * ↑a ^ 4)) * (dens₂ 𝔄).toReal ^ (q⁻¹ - 2⁻¹) * (MeasureTheory.eLpNorm f 2 MeasureTheory.volume).toReal * (MeasureTheory.eLpNorm g 2 MeasureTheory.volume).toReal

Proposition 2.0.3