StepFiveSubWindow

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

t.regularity Step 5: the sub-window re-run of the iteration lemma

References

• ABK26, t.regularity Step 5.

1. The per-scale decay hypothesis, named

def Algsuperdiff.Section4.Provider.Regularity.IterationDecay {d : ℕ} (U : ℤ → Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d → ℝ) (g : ℤ → HCPolySupport.Vec d) (h : ℕ) (θ : ℝ) (ε δ : ℤ → ℝ) (B : Finset ℤ) (n m : ℤ) : Prop

e.Ej.decay.assumption — the per-scale excess-decay hypothesis of l.iteration.lemma, transcribed character for character from the anchor Algsuperdiff.Frozen.Section4.iteration_lemma and given a name, so that it can be quoted as the one input Step 5 takes from Step 4.

For every scale j ∈ [n,m] outside the bad set B, E(u, U_{j-h}) ≤ θ^h E(u, U_j) + ε_j |∇l_j| + δ_j.

Equations

• One or more equations did not get rendered due to their size.

2. Elementary consequences of the window binders

theorem Algsuperdiff.Section4.Provider.Regularity.subset_of_iterationNest {d : ℕ} {U : ℤ → Set (HCPolySupport.Vec d)} {m : ℤ} (hnest : ∀ j ≤ m, U (j - 1) ⊆ U j) {a : ℤ} (b : ℤ) : a ≤ b → b ≤ m → U a ⊆ U b

Nesting U (j-1) ⊆ U j iterates to U a ⊆ U b for a ≤ b ≤ m.

3. Scalar atoms of the budget-inheritance argument

theorem Algsuperdiff.Section4.Provider.Regularity.one_le_exp_of_nonneg {E : ℝ} (hE : 0 ≤ E) : 1 ≤ Real.exp E

1 ≤ exp E for E ≥ 0, in the form the degenerate case needs.

theorem Algsuperdiff.Section4.Provider.Regularity.le_exp_mul_add_of_nonneg {A S E : ℝ} (hA : 0 ≤ A) (hS : 0 ≤ S) (hE : 0 ≤ E) : A ≤ Real.exp E * (A + S)

The trivial sub-window bound at a degenerate window n' = m': with A ≥ 0, S ≥ 0 and E ≥ 0 one has A ≤ e^E (A + S). Kept as an abstract-real atom so that exp never meets the geometry.

theorem Algsuperdiff.Section4.Provider.Regularity.exp_mul_le_exp_mul {E E' X X' : ℝ} (hEE : E' ≤ E) (hXX : X' ≤ X) (hX' : 0 ≤ X') : Real.exp E' * X' ≤ Real.exp E * X

The prefactor/budget comparison, with exp isolated: a smaller exponent and a smaller nonnegative second factor give a smaller product.

4. The sub-window device

theorem Algsuperdiff.Section4.Provider.Regularity.exists_oscillation_subwindow_of_iterationLemma (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)), IterationWindowFamily U m → ∀ (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, Support.IsAffineMinimizer (U j) u (c j) (g j)) → IterationDecay U u g h θ ε δ B n m → ∀ (n' m' : ℤ), n ≤ n' → n' ≤ m' → m' ≤ m → (3 ^ (-n') * 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') * Support.normalizedL2On (U m') fun (x : HCPolySupport.Vec d) => u x - HCPolySupport.volumeAverage (U m') u) + ∑ j ∈ Finset.Icc n m, δ j)

The sub-window device. The frozen iteration anchor, conclusion (i), re-exported at every sub-window [n', m'] ⊆ [n, m] with the outer budgets |𝓑|, ∑_{Icc n m} ε and ∑_{Icc n m} δ in place of the sub-window's own.

This is the exact statement the manuscript uses ("The iteration lemma now yields, for every n', m' ∈ ℤ with n ≤ n' ≤ m' ≤ m") and the exact statement l.iteration.lemma does NOT literally provide. The constant C is the anchor's own.

Note the window binder is relaxed from the anchor's n < m to n ≤ m: the degenerate windows are handled by le_exp_mul_add_of_nonneg.