theorem
third_exception_rearrangement
{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]
:
(∑' (n : ℕ) (k : ℕ),
if k ≤ n then ∑' (j : ℕ), ↑(C5_2_9 X n) * 2 ^ (9 * ↑a - ↑j) * 2 ^ (n + k + 3) * MeasureTheory.volume G else 0) = ∑' (k : ℕ),
2 ^ (9 * a + 4 + 2 * k) * ↑(defaultD a) ^ (1 - defaultκ a * ↑(defaultZ a) * (↑k + 1)) * MeasureTheory.volume G * ∑' (n : ℕ), if k ≤ n then (2 * ↑(defaultD a) ^ (-defaultκ a * ↑(defaultZ a))) ^ (↑n - ↑k) else 0
A rearrangement for Lemma 5.2.9 that does not require the tile structure.
Section 5.2 and Lemma 5.1.1 #
theorem
john_nirenberg_aux1
{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)]
{k : ℕ}
{n : ℕ}
{l : ℕ}
{x : X}
{L : Grid X}
(mL : L ∈ Grid.maxCubes (MsetA l k n))
(mx : x ∈ setA (l + 1) k n)
(mx₂ : x ∈ L)
:
Equation (5.2.7) in the proof of Lemma 5.2.5.
theorem
john_nirenberg_aux2
{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)]
{k : ℕ}
{n : ℕ}
{l : ℕ}
{L : Grid X}
(mL : L ∈ Grid.maxCubes (MsetA l k n))
:
Equation (5.2.11) in the proof of Lemma 5.2.5.
def
layervol
{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)]
(k : ℕ)
(n : ℕ)
(t : ℝ)
:
The volume of a "layer" in the key function of Lemma 5.2.7.
Equations
Instances For
theorem
layervol_eq_zero_of_lt
{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)]
{k : ℕ}
{n : ℕ}
{t : ℝ}
(ht : ↑(𝔐 k n).toFinset.card < t)
:
theorem
boundary_exception
{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)]
{k : ℕ}
{n : ℕ}
{l : ℕ}
{u : 𝔓 X}
(hu : u ∈ 𝔘₁ k n l)
:
Lemma 5.2.9