StepFiveIterationResult

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

t.regularity Step 5: e.oscillation.iteration.result

The target

   3^{-n'} ‖u - (u)_{U_{n'}}‖_{L²(U_{n'})}
     ≤ C exp( C₁^{-1} C (1-α)(m-n) )
         ( 3^{-m'} ‖u - (u)_{U_{m'}}‖_{L²(U_{m'})} + C · dataG )
       + C exp( C₁^{-1} C (1-α)(m-n) ) · dataH

for every n', m' ∈ ℤ with n ≤ n' ≤ m' ≤ m. The right-hand shape is fixed by what Step 6 consumes: oscillationHolderBound_of_iterationResult's hiter slot, at Real.exp ((stepOne d Cedos Cann Citer k)⁻¹ * Citer * stepSixExponent alpha n m). The theorem below produces literally that expression.

Four readings of the printed step, and where each is discharged

• The iteration lemma concludes only at the bottom index; the "for every n', m'" conclusion is the sub-window re-run with inherited budgets. Device: StepFiveSubWindow's exists_oscillation_subwindow_of_iterationLemma, applied here.
• The anchor demands the decay on [n,m] \ 𝓑, while Step 4 supplies it only on [n+k, m-1] \ 𝓑_z. Device: stepFiveBadSet below, 𝓑 := (𝓑_z ∪ [n, n+k) ∪ {m}) ∩ [n,m], with |𝓑| ≤ |𝓑_z| + k + 1 (stepFiveBadSet_card_le) priced through the anchor's own exp(C(h+1)(|𝓑|+1)). The enlargement is carried explicitly.
• The boundary leg ε_j ‖∇h‖_{L^∞} 1_{z∉□_{m-1}} sits inside δ_j; it is never discarded — it travels in dataH, whose coefficient is tracked separately from dataG's.
• Only conclusion (i) of the anchor (the product form) is consumed, via the sub-window device, which itself takes only .1.

What is discharged inside, and the one conditional input

The one conditional input is the Step-4 per-scale excess decay, carried as the hypothesis named hstep4 and named in the theorem's name. Its exact text is quoted in the theorem's docstring.

References

• ABK26, t.regularity Step 5.

1. The enlarged bad set

def Algsuperdiff.Section4.Provider.Regularity.stepFiveBadSet (Bz : Finset ℤ) (n m : ℤ) (k : ℕ) : Finset ℤ

The missing indices are exactly [n, n+k) and {m}, so

   𝓑 := ( 𝓑_z ∪ [n, n+k) ∪ {m} ) ∩ [n, m] .

The intersection with [n,m] is what makes 𝓑 ⊆ Finset.Icc n m hold with no side condition on k versus m-n.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepFiveBadSet Bz n m k = (Bz ∪ Finset.Ico n (n + ↑k) ∪ {m}) ∩ Finset.Icc n m

theorem Algsuperdiff.Section4.Provider.Regularity.stepFiveBadSet_subset (Bz : Finset ℤ) (n m : ℤ) (k : ℕ) : stepFiveBadSet Bz n m k ⊆ Finset.Icc n m

The enlarged bad set satisfies the anchor's binder 𝓑 ⊆ Finset.Icc n m.

theorem Algsuperdiff.Section4.Provider.Regularity.stepFiveBadSet_card_le (Bz : Finset ℤ) (n m : ℤ) (k : ℕ) : (stepFiveBadSet Bz n m k).card ≤ Bz.card + k + 1

The enlargement's cardinality price: |𝓑| ≤ |𝓑_z| + k + 1, which the anchor's prefactor exp(C(h+1)(|𝓑|+1)) absorbs.

theorem Algsuperdiff.Section4.Provider.Regularity.iterationDecay_of_stepFourDecay {d : ℕ} {U : ℤ → Set (HCPolySupport.Vec d)} {u : HCPolySupport.Vec d → ℝ} {g : ℤ → HCPolySupport.Vec d} {θ : ℝ} {ε δ : ℤ → ℝ} {Bz : Finset ℤ} {n m : ℤ} {k : ℕ} (hstep4 : ∀ (j : ℤ), n + ↑k ≤ j → j ≤ m - 1 → j ∉ Bz → Support.affineExcess (U (j - ↑k)) u ≤ θ ^ k * Support.affineExcess (U j) u + ε j * Support.slopeMagnitude (g j) + δ j) : IterationDecay U u g k θ ε δ (stepFiveBadSet Bz n m k) n m

2. The contraction parameters θ = 3^{-1/4}, h = k

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepFiveTheta : ℝ

θ := 3^{-1/4}, the iteration lemma's contraction ratio at Step 5.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepFiveTheta = 3 ^ (-(1 / 4))

theorem Algsuperdiff.Section4.Provider.Regularity.stepFiveTheta_mem : stepFiveTheta ∈ Set.Ioo 0 1

θ ∈ (0,1) — the anchor's first θ-binder.

theorem Algsuperdiff.Section4.Provider.Regularity.stepFiveTheta_pow (k : ℕ) : stepFiveTheta ^ k = 3 ^ (-(1 / 4) * ↑k)

θ^k = 3^{-k/4}: the natural-power/rpow bridge the anchor's second θ-binder needs.

theorem Algsuperdiff.Section4.Provider.Regularity.three_rpow_neg_half_lt : 3 ^ (-(1 / 2)) < 3 / 5

3^{-1/2} < 3/5, i.e. 25 < 27.

theorem Algsuperdiff.Section4.Provider.Regularity.stepFiveTheta_pow_mem {k : ℕ} (hk : 2 ≤ k) : stepFiveTheta ^ k ∈ Set.Ioo 0 (3 / 5)

θ^k ∈ (0, 3/5) for k ≥ 2 — the anchor's second θ-binder. The Step-1 integer k is at least 10, so it meets the binder a fortiori.

3. The prefactor conversion, over abstract reals

theorem Algsuperdiff.Section4.Provider.Regularity.exp_budget_bound {C0 hR Bc Se K1 K2 K3 X : ℝ} (hC0 : 0 ≤ C0) (hhR : 0 ≤ hR) (hB : Bc + 1 ≤ K1 + K2 * X) (hS : Se ≤ K3 * X) : C0 * (hR + 1) * (Bc + 1) + C0 * Se ≤ C0 * (hR + 1) * K1 + (C0 * (hR + 1) * K2 + C0 * K3) * X

The additive budget bound behind the prefactor conversion: with |𝓑|+1 ≤ K₁ + K₂ X and ∑ε ≤ K₃ X,

   C₀(h+1)(|𝓑|+1) + C₀ ∑ε  ≤  C₀(h+1)K₁ + ( C₀(h+1)K₂ + C₀K₃ ) X .

Abstract reals only.

theorem Algsuperdiff.Section4.Provider.Regularity.exp_budget_le_mul_exp {C0 hR Bc Se K1 K2 K3 X : ℝ} (hC0 : 0 ≤ C0) (hhR : 0 ≤ hR) (hB : Bc + 1 ≤ K1 + K2 * X) (hS : Se ≤ K3 * X) : Real.exp (C0 * (hR + 1) * (Bc + 1) + C0 * Se) ≤ Real.exp (C0 * (hR + 1) * K1) * Real.exp ((C0 * (hR + 1) * K2 + C0 * K3) * X)

The exponential form of the same: the anchor's ADDITIVE prefactor is dominated by a times exp of the Step-6 exponent.

4. The shape of e.oscillation.iteration.result, over abstract reals

theorem Algsuperdiff.Section4.Provider.Regularity.oscillation_shape_aux {C Cpre Cg Ch Eq Q oscLo oscHi dataG dataH Sd : ℝ} (hEq : 0 ≤ Eq) (hQ : 0 ≤ Q) (hoscHi : 0 ≤ oscHi) (hdataG : 0 ≤ dataG) (hdataH : 0 ≤ dataH) (hCg0 : 0 ≤ Cg) (hCh0 : 0 ≤ Ch) (hSd : Sd ≤ Cg * dataG + Ch * dataH) (hpre : Eq ≤ Cpre * Q) (hCpre : Cpre ≤ C) (hCgC : Cpre * Cg ≤ C * C) (hChC : Cpre * Ch ≤ C) (hiter : oscLo ≤ Eq * (oscHi + Sd)) : oscLo ≤ C * Q * (oscHi + C * dataG) + C * Q * dataH

The scalar core of the composition into Step 6's hiter shape: no exp, no rpow, every atom an abstract real. Eq is the anchor's prefactor, Q the Step-6 exponential, Sd the δ-sum.