StepOneWindow

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

D₁ as a geometric window sum of the collapsed kick family

ABK26, §4.2, Step 1 of l.minimal.scale.sep. This module proves the identity that makes D₁ a Step-1 object at all, and the pointwise estimate that turns it into a geometric window sum of the collapsed kick variable:

D₁(k) = s^{1/2} 1_{𝒢(k;s,1)} ∑_{p ≥ 0} 3^{−½sp} · annularKick_{k−p}   (the IDENTITY)
      ≤ s^{1/2} ∑_{p ≥ 0} 3^{−¼sp} · X_{k−p}                       (the ESTIMATE)

(the estimate is ABK26)

The weight-bridging identity

The anchor's clause-(i) annular group carries the weights 3^{−s(m−n)} indexed by the pair (j, n) with n ≤ j−1 ≤ m−1; after the √-halving of DDecomposition.lean the weights are 3^{−½s(k−n)}. KickFamily's annularKick_j is the inner-scale sum at the weight 3^{−½s(j−i)}. The two meet through the exact factorisation

3^{−½s(k−n)} = 3^{−½s(k−j)} · 3^{−½s(j−n)}                (annularHalfSum_eq_tsum)

so that annularHalfSum_k = ∑_{p ≥ 0} 3^{−½sp} annularKick_{k−p} as an identity of ℝ≥0∞ — nothing is dropped, no convergence is used, and the halved exponent of the outer sum is exactly the halved exponent of that weight. There is NO weight mismatch: annularKick sits at the §4.2 weight 3^{−½s·} precisely because the §4.1 lane's 3^{−¼s·} weight is squared and §4.2's is not.

Main definitions

• outerScaleEquiv — the ℕ-enumeration p ↦ k − p of the outer scales j ≤ k.
• windowKickSum — the geometric window sum ∑_p 3^{−¼sp} X_{k−p}, in ℝ, at the collapse coefficient supplied by the caller.

Main results

• annularHalfSum_eq_tsum — the weight-bridging identity.
• summable_windowKick_of_mem_eventG2 — the window sum converges on the good event (the crude majorant √√y ≤ 2 + y suffices; no sharp estimate is needed here).
• dOne_le_ofReal_windowKickSum — the Step-1 pointwise estimate, at every sample: off the good event the left side is 0, on it the collapse step applies.
• dOne_ne_top — D₁(k) is finite at every sample, so it may be read in ℝ.

References

• ABK26, l.minimal.scale.sep, Step 1.

1. The unsquared lattice supremum equals the Finset maximum

theorem Algsuperdiff.Section4.Provider.MinimalScale.iSup_ofReal_annularErrorObservable_eq {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {j n : ℤ} (hn : n ≤ j) (omega : Section3.Cutoff.CutoffSample d) : ⨆ (v : ↑(Support.latticeAnnulusSet d n j (j - 1))), ENNReal.ofReal (Support.annularErrorObservable M n s (Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint n ↑v) omega)) = ENNReal.ofReal (kickAnnMax M s j n omega)

The unsquared companion of Proportion.errorAnnSup_eq_ofReal_errorAnnMax: the ℝ≥0∞ supremum over the lattice annulus S agrees with the 0-floored Finset maximum kickAnnMax.

2. The ℕ-enumeration of the outer scales

def Algsuperdiff.Section4.Provider.MinimalScale.outerScaleEquiv (k : ℤ) : ℕ ≃ { j : ℤ // j ≤ k }

The outer scales j ≤ k, enumerated by the offset p = k − j.

Equations

• Algsuperdiff.Section4.Provider.MinimalScale.outerScaleEquiv k = { toFun := fun (p : ℕ) => ⟨k - ↑p, ⋯⟩, invFun := fun (j : { j : ℤ // j ≤ k }) => (k - ↑j).toNat, left_inv := ⋯, right_inv := ⋯ }

3. The weight-bridging identity

theorem Algsuperdiff.Section4.Provider.MinimalScale.three_rpow_half_eq_weightThird (a : ℝ) {x : ℤ} (hx : 0 ≤ x) : Real.rpow 3 (-(1 / 2) * a * ↑x) = Proportion.weightThird (a / 2) x.toNat

The halved weight at a nonnegative offset, in weightThird form.

theorem Algsuperdiff.Section4.Provider.MinimalScale.annularHalfSum_eq_tsum {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (k : ℤ) (omega : Section3.Cutoff.CutoffSample d) : annularHalfSum M s k omega = ∑' (p : ℕ), ENNReal.ofReal (Proportion.weightThird (↑s / 2) p) * annularKickE M s (k - ↑p) omega

The weight-bridging identity. The halved annular group of the D-decomposition IS the geometric window sum of the inner-scale sums:

annularHalfSum_k = ∑_{p ≥ 0} 3^{−½sp} · annularKick_{k−p} .

An equality of ℝ≥0∞: the whole content is the exponent factorisation 3^{−½s(k−n)} = 3^{−½s(k−j)}·3^{−½s(j−n)}.

4. The geometric window sum

noncomputable def Algsuperdiff.Section4.Provider.MinimalScale.windowKickSum {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (lam K : ℝ) (k : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ℝ

The geometric window sum: ∑_{p ≥ 0} 3^{−¼sp} X_{k−p}, formed in ℝ at the quarter rate. The weight is written exactly as Probability.window_geom_head_rearrange writes it.

Equations

• Algsuperdiff.Section4.Provider.MinimalScale.windowKickSum M s lam K k omega = ∑' (p : ℕ), 3 ^ (-(↑s / 4 * ↑p)) * Algsuperdiff.Section4.Provider.MinimalScale.kickCollapsed M s lam K (k - ↑p) omega

theorem Algsuperdiff.Section4.Provider.MinimalScale.windowKickSum_nonneg {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {lam : ℝ} (hlam : 0 ≤ lam) (K : ℝ) (k : ℤ) (omega : Section3.Cutoff.CutoffSample d) : 0 ≤ windowKickSum M s lam K k omega

theorem Algsuperdiff.Section4.Provider.MinimalScale.windowKickSum_eq {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (lam K : ℝ) (k : ℤ) (omega : Section3.Cutoff.CutoffSample d) : windowKickSum M s lam K k omega = ∑' (p : ℕ), Proportion.weightThird (↑s / 4) p * kickCollapsed M s lam K (k - ↑p) omega

The window sum, in the weightThird rendering.

theorem Algsuperdiff.Section4.Provider.MinimalScale.sqrt_sqrt_le_two_add {y : ℝ} (hy : 0 ≤ y) : √√y ≤ 2 + y

√√y ≤ 2 + y — the crude majorant that makes the window sum summable without any sharp estimate.

theorem Algsuperdiff.Section4.Provider.MinimalScale.summable_weightThird {a : ℝ} (ha : 0 < a) : Summable fun (p : ℕ) => Proportion.weightThird a p

theorem Algsuperdiff.Section4.Provider.MinimalScale.summable_windowKick_of_mem_eventG2 {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {k : ℤ} {lam K : ℝ} (hlam : 0 ≤ lam) (hK : 0 ≤ K) (hs1 : ↑s ≤ 1) {omega : Section3.Cutoff.CutoffSample d} (hmem : omega ∈ Support.eventG2 M k s 1) : Summable fun (p : ℕ) => Proportion.weightThird (↑s / 4) p * kickCollapsed M s lam K (k - ↑p) omega

The window sum converges on the good event. The crude majorant X ≤ lam + 2 + K·annularKick and the good-event bound reduce this to two geometric series (rates ¼s and ⅛s).

5. The Step-1 pointwise estimate

theorem Algsuperdiff.Section4.Provider.MinimalScale.dOne_le_ofReal_windowKickSum {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (Ccg : ℝ) {k : ℤ} {lam K : ℝ} (hlam : 0 ≤ lam) (hs1 : ↑s ≤ 1) (hK : 216 * (√↑s ^ 9)⁻¹ ≤ K) (omega : Section3.Cutoff.CutoffSample d) : dOne M Ccg s k omega ≤ ENNReal.ofReal (√↑s * windowKickSum M s lam K k omega)

The Step-1 pointwise estimate, at every sample.

D₁(k) ≤ s^{1/2} ∑_{p ≥ 0} 3^{−¼sp} X_{k−p} .

Off the good event the left side is 0 and there is nothing to prove; on it the identity annularHalfSum_eq_tsum reduces the claim to the collapse step weighted_annularKick_le_kickCollapsed, termwise in p.

theorem Algsuperdiff.Section4.Provider.MinimalScale.dOne_ne_top {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (Ccg : ℝ) {k : ℤ} (hs1 : ↑s ≤ 1) (omega : Section3.Cutoff.CutoffSample d) : dOne M Ccg s k omega ≠ ⊤

D₁(k) is finite at every sample, so it may be read in ℝ without a junk-value hazard. This is what lets the final Cesàro assembly move between ℝ≥0∞ and ℝ.

theorem Algsuperdiff.Section4.Provider.MinimalScale.dOne_toReal_le {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (Ccg : ℝ) {k : ℤ} {lam K : ℝ} (hlam : 0 ≤ lam) (hs1 : ↑s ≤ 1) (hK : 216 * (√↑s ^ 9)⁻¹ ≤ K) (omega : Section3.Cutoff.CutoffSample d) : (dOne M Ccg s k omega).toReal ≤ √↑s * windowKickSum M s lam K k omega

The real reading of the Step-1 pointwise estimate.

6. Reading the window sum at the kick family's OWN coefficient

The collapse step needs the coefficient K' ≥ 216 s^{−9/2}, while K1's Γ₂ tail and first moment are supplied at K1's own C s^{−9/2}. The two are reconciled by the fourth root of the ratio — a dimensional constant — so that the Cesàro engine below is fed the family K1 actually estimates.

theorem Algsuperdiff.Section4.Provider.MinimalScale.windowKickSum_le_mul_of_coeff_le {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {k : ℤ} {lam K K' : ℝ} (hlam : 0 ≤ lam) (hK : 0 < K) (hKK : K ≤ K') (hs1 : ↑s ≤ 1) {omega : Section3.Cutoff.CutoffSample d} (hmem : omega ∈ Support.eventG2 M k s 1) : windowKickSum M s lam K' k omega ≤ √√(K' / K) * windowKickSum M s lam K k omega

The window sum is monotone in the collapse coefficient, up to the fourth root of the ratio (good-event version: both sums converge there).

theorem Algsuperdiff.Section4.Provider.MinimalScale.dOne_toReal_le_scaled {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (Ccg : ℝ) {k : ℤ} {lam K K' : ℝ} (hlam : 0 ≤ lam) (hs1 : ↑s ≤ 1) (hK : 0 < K) (hKK : K ≤ K') (hK' : 216 * (√↑s ^ 9)⁻¹ ≤ K') (omega : Section3.Cutoff.CutoffSample d) : (dOne M Ccg s k omega).toReal ≤ √↑s * (√√(K' / K) * windowKickSum M s lam K k omega)

The Step-1 pointwise estimate at the kick family's own coefficient, at every sample: D₁(k) ≤ s^{1/2} ρ ∑_p 3^{−¼sp} X_{k−p} with X the collapsed variable at the coefficient K and ρ = (K'/K)^{1/4} for any admissible K' ≥ 216 s^{−9/2}.