StepFourFinalBudget

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

theorem Algsuperdiff.Section4.Provider.Regularity.oscillationIterationResult_of_stepFourDecay_generic (d : ℕ) (hd : d ≠ 0) (k : ℕ) (hk : 2 ≤ k) {Ceps : ℝ} (hCeps : 0 ≤ Ceps) : ∃ (C : ℝ) (Citer : ℝ), 0 < C ∧ 0 ≤ Citer ∧ ∀ (Cedos Cann alpha : ℝ), alpha ≤ 1 → ∀ (n m : ℤ), 1 ≤ m - n → ∀ (U : ℤ → Set (HCPolySupport.Vec d)), IterationWindowFamily U m → ∀ (u : HCPolySupport.Vec d → ℝ), MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (U m)) → ∀ (c : ℤ → ℝ) (g : ℤ → HCPolySupport.Vec d), (∀ j ≤ m, Support.IsAffineMinimizer (U j) u (c j) (g j)) → ∀ (Bz : Finset ℤ), ↑Bz.card ≤ stepOneDelta (stepOneC1 d Cedos Cann Citer k) alpha * (↑m - ↑n + 1) → ∀ (ε δ : ℤ → ℝ), (∀ (j : ℤ), n ≤ j → j ≤ m → 0 ≤ ε j) → (∀ (j : ℤ), n ≤ j → j ≤ m → 0 ≤ δ j) → ∑ j ∈ Finset.Icc n m, ε j ≤ 2 * Ceps * stepOneDelta (stepOneC1 d Cedos Cann Citer k) alpha * (↑m - ↑n) → ∀ (dataG dataH : ℝ), 0 ≤ dataG → 0 ≤ dataH → ∑ j ∈ Finset.Icc n m, δ j ≤ dataG + dataH → (∀ (j : ℤ), n + ↑k ≤ j → j ≤ m - 1 → j ∉ Bz → Support.affineExcess (U (j - ↑k)) u ≤ stepFiveTheta ^ k * Support.affineExcess (U j) u + ε j * Support.slopeMagnitude (g j) + δ j) → ∀ (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) ≤ C * Real.exp ((stepOneC1 d Cedos Cann Citer k)⁻¹ * Citer * stepSixExponent alpha n m) * ((3 ^ (-m') * Support.normalizedL2On (U m') fun (x : HCPolySupport.Vec d) => u x - HCPolySupport.volumeAverage (U m') u) + C * dataG) + C * Real.exp ((stepOneC1 d Cedos Cann Citer k)⁻¹ * Citer * stepSixExponent alpha n m) * dataH

e.oscillation.iteration.result with the ε-budget slot generic ('s mismatch (1), fixed's own price): the ε-sum is allowed the constant 2 C_ε and the produced iteration constant becomes C_iter = 2 C₀ (k + 1 + C_ε). At C_ε = 1 this is the pinned iteration result verbatim.

2. The δ-budget of the interior family

theorem Algsuperdiff.Section4.Provider.Regularity.edFinalDeltaConst_nonneg (d : ℕ) [NeZero d] {C : ℝ} (hC : 0 ≤ C) (k : ℕ) {s : ℝ} (hs : 0 ≤ s) : 0 ≤ edFinalDeltaConst d C k s

noncomputable def Algsuperdiff.Section4.Provider.Regularity.edFinalKgTop {d : ℕ} (M : Section3.ABKModel d) (Cdel Kg : ℝ) (m : ℤ) : ℝ

The top-scale constant of the interior δ-budget, 4 C_δ 3^{m/2} σ_m^{-1} K_g.

Equations

• Algsuperdiff.Section4.Provider.Regularity.edFinalKgTop M Cdel Kg m = 4 * Cdel * (3 ^ (↑m / 2) * (↑(Algsuperdiff.Section3.Annealed.sigmaBar M m))⁻¹) * Kg

noncomputable def Algsuperdiff.Section4.Provider.Regularity.edFinalDataG {d : ℕ} (M : Section3.ABKModel d) (Cdel Kg : ℝ) (m : ℤ) : ℝ

dataG for the interior branch: 4 C_δ 3^{m/2} σ_m^{-1} K_g / (1 - 3^{-(1/2-γ)}). There is no dataH — the interior clause has no ∇h leg.

Equations

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

theorem Algsuperdiff.Section4.Provider.Regularity.edFinalDataG_nonneg {d : ℕ} {M : Section3.ABKModel d} (hgamma : M.gamma < 1 / 2) {Cdel Kg : ℝ} (hC : 0 ≤ Cdel) (hK : 0 ≤ Kg) (m : ℤ) : 0 ≤ edFinalDataG M Cdel Kg m

theorem Algsuperdiff.Section4.Provider.Regularity.edFinalDelta_le_zpow {d : ℕ} {M : Section3.ABKModel d} {m0 : ℤ} {Ecap : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 Ecap) {Cdel Kg : ℝ} (hC : 0 ≤ Cdel) (hK : 0 ≤ Kg) {j m : ℤ} (hjm : j ≤ m) (hm : m ≤ m0) : edFinalDelta M Cdel Kg j ≤ edFinalKgTop M Cdel Kg m * stepFiveRatioG M ^ (m - j)

theorem Algsuperdiff.Section4.Provider.Regularity.sum_Icc_top_edFinalDelta_le {d : ℕ} {M : Section3.ABKModel d} {m0 : ℤ} {Ecap : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 Ecap) (hgamma : M.gamma < 1 / 2) {Cdel Kg : ℝ} (hC : 0 ≤ Cdel) (hK : 0 ≤ Kg) {n m : ℤ} (hnm : n ≤ m) (hm : m ≤ m0) : ∑ j ∈ Finset.Icc n m, edFinalDelta M Cdel Kg j ≤ edFinalDataG M Cdel Kg m

e.sum.delta.j.bound for the interior family, on the anchor's own window [n,m].

3. The ε-budget at the produced coefficient

theorem Algsuperdiff.Section4.Provider.Regularity.sum_Icc_edFinalEps_le {d : ℕ} {M : Section3.ABKModel d} {delta Ceps : ℝ} {n m : ℤ} {omega : Section3.Cutoff.CutoffSample d} (hCeps : 0 ≤ Ceps) (hdelta : 0 ≤ delta) (hwin : 14 ≤ m - n) (hgood : GoodScaleWindows M stepOneSEighth delta stepOneSEighth_pos n m omega) {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) : ∑ j ∈ Finset.Icc n m, Ceps * stepFiveEps M j (Support.triadicLatticePoint n v) delta omega ≤ 2 * Ceps * delta * (↑m - ↑n)

e.sum.eps.j.bound at the collapse's own coefficient: ∑ C_ε ε_j ≤ 2 C_ε δ (m-n), the slot of the generic re-run.