Equations
- ShortVariables.termNnq' = Lean.ParserDescr.node `ShortVariables.termNnq' 1024 (Lean.ParserDescr.symbol "nnq'")
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)
:
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)
:
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
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 : 𝔓 X) => x1 ≤ x2) 𝔄)
:
‖∫ (x : X), (starRingEnd ℂ) (g x) * carlesonSum 𝔄 f x‖ₑ ≤ ↑(C_2_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}
(hf : Measurable f)
(h2f : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x)
(hA : A ⊆ G)
(h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) 𝔄)
:
Version of the forest 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}
(hf : Measurable f)
(h2f : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x)
(hA : A ⊆ G)
(h𝔄 : IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) 𝔄)
:
Version of the forest 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.