theorem
third_exception_rearrangement
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F 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
dense_cover
{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)]
(k : ℕ)
:
Lemma 5.2.2
theorem
john_nirenberg_aux1
{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)]
{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 → ℤ}
{F 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.
theorem
john_nirenberg
{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)]
{k n l : ℕ}
:
Lemma 5.2.5
def
layervol
{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)]
(k n : ℕ)
(t : ℝ)
:
The volume of a "layer" in the key function of Lemma 5.2.7.
Equations
Instances For
theorem
lintegral_Ioc_layervol_one
{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)]
{k n l : ℕ}
:
theorem
lintegral_Ioc_layervol_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)]
{k n a✝ b : ℕ}
:
theorem
top_tiles_aux
{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)]
{k n : ℕ}
:
theorem
tree_count
{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)]
{k n j : ℕ}
{x : X}
:
Lemma 5.2.8
theorem
third_exception_aux
{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)]
{k n j : ℕ}
: