IterationLemma #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The iteration lemma — [ABK] l.iteration.lemma #
A one-step affine excess decay by a factor theta^h, valid at every scale
outside a bad set B, iterates across the whole range of scales. The two
conclusions are a normalized L^2 oscillation bound and an affine excess
bound at the bottom scale, both losing only exp(C (h+1)(|B|+1)) and an
additive theta-power for the bad scales, plus the accumulated defects.
Proved; reduces to the standard axioms.
theorem
Algsuperdiff.Frozen.Section4.iteration_lemma
(d : ℕ)
(hd : d ≠ 0)
:
∃ (C : ℝ),
0 < C ∧ ∀ (h : ℕ),
∀ θ ∈ Set.Ioo 0 1,
θ ^ h ∈ Set.Ioo 0 (3 / 5) →
∀ (n m : ℤ),
n < m →
∀ (U : ℤ → Set (HCPolySupport.Vec d)),
(∀ j ≤ m, MeasurableSet (U j)) →
(∀ j ≤ m, U (j - 1) ⊆ U j) →
(∀ j ≤ m,
∃ (x : HCPolySupport.Vec d) (y : HCPolySupport.Vec d),
(fun (v : HCPolySupport.Vec d) => x + v) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (j - 2)) ⊆
U j ∧ U j ⊆
(fun (v : HCPolySupport.Vec d) => y + v) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d j)) →
∀ (u : HCPolySupport.Vec d → ℝ),
MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (U m)) →
∀ B ⊆ Finset.Icc n m,
∀ (ε δ : ℤ → ℝ),
(∀ (j : ℤ), n ≤ j → j ≤ m → 0 ≤ ε j) →
(∀ (j : ℤ), n ≤ j → j ≤ m → 0 ≤ δ j) →
∀ (c : ℤ → ℝ) (g : ℤ → HCPolySupport.Vec d),
(∀ j ≤ m, Section4.Support.IsAffineMinimizer (U j) u (c j) (g j)) →
(∀ (j : ℤ),
n ≤ j →
j ≤ m →
j ∉ B →
Section4.Support.affineExcess (U (j - ↑h)) u ≤ θ ^ h * Section4.Support.affineExcess (U j) u + ε j * Section4.Support.slopeMagnitude (g j) + δ j) →
(3 ^ (-n) * Section4.Support.normalizedL2On (U n) fun (x : HCPolySupport.Vec d) =>
u x - HCPolySupport.volumeAverage (U n) u) ≤ Real.exp (C * (↑h + 1) * (↑B.card + 1) + C * ∑ j ∈ Finset.Icc n m, ε j) * ((3 ^ (-m) * Section4.Support.normalizedL2On (U m) fun (x : HCPolySupport.Vec d) =>
u x - HCPolySupport.volumeAverage (U m) u) + ∑ j ∈ Finset.Icc n m, δ j) ∧ ∀ (M : ℝ),
(∀ (j : ℤ), n ≤ j → j ≤ m → ε j ≤ M) →
Section4.Support.affineExcess (U n) u ≤ θ.rpow (-(C * (↑h + 1) * (↑B.card + 1))) * Real.exp
(C * (↑h + 1) * (↑B.card + 1) + C * ∑ j ∈ Finset.Icc n m, ε j) * (θ ^ (m - n) * Section4.Support.affineExcess (U m) u + M * (3 ^ (-m) * Section4.Support.normalizedL2On (U m)
fun (x : HCPolySupport.Vec d) =>
u x - HCPolySupport.volumeAverage (U m) u) + (1 + M) * ∑ j ∈ Finset.Icc n m, δ j)