def ShortVariables.termNnq' : Lean.ParserDescr

Equations

• ShortVariables.termNnq' = Lean.ParserDescr.node `ShortVariables.termNnq' 1024 (Lean.ParserDescr.symbol "nnq'")

theorem nnq'_coe {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] : 2 * ↑(nnq X) / (↑(nnq X) + 1) = 2 * ↑(nnq X) / (↑(nnq X) + 1)

theorem one_lt_nnq' {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] : 1 < 2 * nnq X / (nnq X + 1)

theorem one_lt_nnq'_coe {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] : 1 < 2 * ↑(nnq X) / (↑(nnq X) + 1)

theorem nnq'_lt_nnq {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] : 2 * nnq X / (nnq X + 1) < nnq X

theorem nnq'_lt_nnq_coe {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] : 2 * ↑(nnq X) / (↑(nnq X) + 1) < ↑(nnq X)

theorem nnq'_lt_two {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] : 2 * nnq X / (nnq X + 1) < 2

theorem nnq'_lt_two_coe {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] : 2 * ↑(nnq X) / (↑(nnq X) + 1) < 2

theorem E_disjoint {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)] {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) ↑𝔄) {p 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 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 → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {x y : X} {𝔄 : Set (𝔓 X)} (p : ↑𝔄) (hxE : x ∈ E ↑p) (hy : Ks (𝔰 ↑p) x y ≠ 0) : ‖Ks (𝔰 ↑p) x y‖₊ ≤ 2 ^ (6 * a + 101 * a ^ 3) / MeasureTheory.volume.nnreal (Metric.ball (𝔠 ↑p) (8 * ↑(defaultD a) ^ 𝔰 ↑p))

theorem MaximalBoundAntichain {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)] {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) ↑𝔄) {f : X → ℂ} (hfm : Measurable f) (x : X) : ↑‖∑ p ∈ 𝔄, carlesonOn p f x‖₊ ≤ ↑(C_6_1_2 a) * MB MeasureTheory.volume (↑𝔄) 𝔠 (fun (𝔭 : 𝔓 X) => 8 * ↑(defaultD a) ^ 𝔰 𝔭) f x

theorem Set.eq_indicator_one_mul {X : Type u_1} {F : Set X} {f : X → ℂ} (hf : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) : f = F.indicator 1 * f

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)⁻¹

theorem eLpNorm_maximal_function_le' {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)] {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) ↑𝔄) {f : X → ℂ} (hf : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) (hfm : Measurable f) : MeasureTheory.eLpNorm (fun (x : X) => (maximalFunction MeasureTheory.volume (↑𝔄) 𝔠 (fun (𝔭 : 𝔓 X) => 8 * ↑(defaultD a) ^ 𝔰 𝔭) (2 * (2 * ↑(nnq X) / (↑(nnq X) + 1)) / (3 * (2 * ↑(nnq X) / (↑(nnq X) + 1)) - 2)) f x).toReal) 2 MeasureTheory.volume ≤ 2 ^ (2 * a) * (3 * (2 * ↑(nnq X) / (↑(nnq X) + 1)) - 2) / (2 * (2 * ↑(nnq X) / (↑(nnq X) + 1)) - 2) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

theorem Dens2Antichain {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)] {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) ↑𝔄) (ha : 4 ≤ a) {f : X → ℂ} (hf : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) (hfm : Measurable f) {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 → ℤ} {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 → ℂ} (hf : Measurable f) (hf1 : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) (hg : Measurable g) (hg1 : ∀ (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