FiniteCorridorIteration

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

Finite weighted-defect corridor iteration

This module is a Provider helper: it proves an arithmetic statement about an abstract sequence and makes no source-node status claim.

F t ≤ A δ₁ (δ₁ + 3⁻ᵗ) + C ∑_{k=1}^{t} 3⁻ᵏ (F (t - k) - F t),      t ≥ j₀,

together with the initialization e.iter.init, which supplies the crude O(E²γ) estimate F t ≤ K₀ δ₁ at every scale of the physical corridor `[L, L

• t]. The nonnegativity of the response mean is a *separate* source input, namely J ≥ 0frome.Jenergyv.nosymm; it is not part of the §A.4 display. Only predecessors t - kwith0 ≤ t - k ≤ t` occur, so no value below the cutoff is ever used: that is precisely what replaces the printed bi-infinite iteration.

F (j₀ + j) ≤ K δ₁ (δ₁ + ρ ^ j),      ρ ∈ (0, 1),

where K = finiteCorridorAmplitude A₀ r j₀ and ρ = finiteCorridorDecayRate C are built only from the recurrence data A, C, K₀, j₀ and the geometric weight r. exists_finiteCorridor_weightedDefect_decay states that quantifier order explicitly.

The weight r is kept abstract subject to 0 ≤ r ≤ 1/3. The single parameter r governs BOTH, so r = 3⁻ᵈ is admissible only for a consumer whose lag weights are also 3⁻ᵈᵏ; a consumer holding the source's 3⁻ᵏ lag weights takes r = 1/3 and weakens any sharper forcing decay to 3⁻ᵗ. No instantiation is performed here: the proved exists_relativeCutoff_finiteCorridor_fluctuationVariance_bound (CombineFiniteVariance.lean) is a two-plus-eight variance-channel bound carrying Real.rpow 3 (-d * (n - L).toNat), so passing to a mean recurrence, converting rpow to the natural-number power r ^ t, and checking 3⁻ᵈ ≤ 1/3 (which needs 1 ≤ d) are consumer obligations.

Elementary finite sums

The weighted-defect kernel

def Algsuperdiff.Section3.Provider.Homogenization.WeightedDefectKernel (C r ρ : ℝ) : Prop

The kernel inequality that closes the finite strong induction: it pays for replacing the predecessor weight ρ ^ (j - k) by the current weight ρ ^ j inside the finite lag sum.

Equations

• Algsuperdiff.Section3.Provider.Homogenization.WeightedDefectKernel C r ρ = ∀ (j : ℕ), C * ∑ k ∈ Finset.Icc 1 j, r ^ k * (ρ ^ (j - k) - ρ ^ j) ≤ 1 / 2 * ρ ^ j

The iteration constants

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.finiteCorridorDecayRate (C : ℝ) : ℝ

The geometric rate produced by the finite weighted-defect iteration. It depends only on the defect coefficient C of the recurrence.

Equations

• Algsuperdiff.Section3.Provider.Homogenization.finiteCorridorDecayRate C = 1 - (4 * (C + 1))⁻¹

def Algsuperdiff.Section3.Provider.Homogenization.finiteCorridorAmplitude (A C K₀ r : ℝ) (j₀ : ℕ) : ℝ

The amplitude produced by the finite weighted-defect iteration. It depends only on the forcing coefficient A, the defect coefficient C, the crude initialization coefficient K₀, the geometric weight r and the initial separation j₀ of the recurrence.

Equations

• Algsuperdiff.Section3.Provider.Homogenization.finiteCorridorAmplitude A C K₀ r j₀ = 2 * (A + 2 * K₀ + C * K₀ * ↑j₀ * r)

theorem Algsuperdiff.Section3.Provider.Homogenization.finiteCorridorDecayRate_pos {C : ℝ} (hC : 0 ≤ C) : 0 < finiteCorridorDecayRate C

The rate is positive.

theorem Algsuperdiff.Section3.Provider.Homogenization.finiteCorridorDecayRate_lt_one {C : ℝ} (hC : 0 ≤ C) : finiteCorridorDecayRate C < 1

The rate is a genuine contraction factor.

theorem Algsuperdiff.Section3.Provider.Homogenization.finiteCorridorAmplitude_nonneg {A C K₀ r : ℝ} (j₀ : ℕ) (hA : 0 ≤ A) (hC : 0 ≤ C) (hK₀ : 0 ≤ K₀) (hr0 : 0 ≤ r) : 0 ≤ finiteCorridorAmplitude A C K₀ r j₀

The amplitude is nonnegative.

The unshifted finite iteration

The shifted finite corridor iteration

theorem Algsuperdiff.Section3.Provider.Homogenization.finiteCorridor_weightedDefect_iteration {F : ℕ → ℝ} {A C K₀ δ r : ℝ} {j₀ : ℕ} (hA : 0 ≤ A) (hC : 0 ≤ C) (hK₀ : 0 ≤ K₀) (hδ : 0 ≤ δ) (hr0 : 0 ≤ r) (hr3 : r ≤ 1 / 3) (hFnonneg : ∀ (t : ℕ), 0 ≤ F t) (hcrude : ∀ (t : ℕ), F t ≤ K₀ * δ) (hrec : ∀ (t : ℕ), j₀ < t → F t ≤ A * δ * (δ + r ^ t) + C * ∑ k ∈ Finset.Icc 1 t, r ^ k * (F (t - k) - F t)) (j : ℕ) : F (j₀ + j) ≤ finiteCorridorAmplitude A C K₀ r j₀ * δ * (δ + finiteCorridorDecayRate C ^ j)

F is an arbitrary real sequence; nothing below mentions J, the coefficient field, the cutoff L or the direction e. Under the intended instantiation F t = 𝔼[J(□_{L+t}, σ_L^{-1/2}e, σ_L^{1/2}e; a_L)] the hypotheses read:

• hFnonneg: the response mean is nonnegative. This is NOT part of the §A.4 display; it is the separate source fact J ≥ 0 (e.Jenergyv.nosymm). It is not needed for the truth of the conclusion — truncating F at 0 removes it — and is kept only because it shortens the prefix estimate.
• hcrude: the initialization e.iter.init, i.e. the crude O(E²γ) bound F t ≤ K₀ δ₁, available at every scale of the corridor [L, L + t].
• hrec: the finite pre-extension recurrence, whose lag sum ranges over 1 ≤ k ≤ t only.

Establishing hcrude, hrec, hFnonneg for the actual response mean, and identifying A, C, K₀, j₀, r with dimension-only constants, is consumer work not done here; so is the selection of k₁.