WindowRearrange

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

Window rearrangement of geometric layer tails

ABK26, l.minimal.scale.sep Steps 1 and 2. The minimal-scale separation bound sums, over a window of scales k ∈ [n, m], a geometric layer tail. Upward (Step 2) the tail is ∑_{l ≥ k} 3^{−α(l−k)} Y_l; downward (Step 1) it is ∑_{l ≤ k} 3^{−α(k−l)} X_l. Both rearrange into (1 − 3^{−α})⁻¹ · ∑_{l ∈ [n,m]} Y_l + min(m − n + 1, (1 − 3^{−α})⁻¹) · (tail),

i.e. a window part carrying the geometric constant Cgeo = (1 − 3^{−α})⁻¹ and an off-window part carrying the sharper coefficient min(window length, Cgeo). The min is load-bearing: in the short-window regime m − n < α⁻¹ the crude Cgeo on the off-window term loses a power of the parameter and the printed envelope fails.

Main results

• Algsuperdiff.Probability.window_geom_tail_rearrange — the upward headline, with the min coefficient on the off-window tail.
• Algsuperdiff.Probability.window_geom_tail_rearrange_le — the crude Cgeo-on-both-terms corollary.
• Algsuperdiff.Probability.window_geom_head_rearrange — the downward (below-window) reflection.

Design

Everything here is pure deterministic real analysis: no probability, no measure theory, no summability hypothesis, and the import closure is Mathlib only. The statements are unconditional in the layer field (only nonnegativity is assumed), which forces an honest treatment of the tsum junk value: if the off-window family fails to be summable then every layer tail on the left also fails (the families differ by a finite prefix and a positive geometric rescaling), so both sides degenerate and the inequality is trivial.

In the summable case the proof is a finite induction on the window length, using the exact one-step recursion T k = Y k + 3^{−α} · T (k+1) for the layer tail T k = ∑_j 3^{−αj} Y (k+j). The inductive invariant keeps the tail coefficient as the partial geometric sum 3^{−α} · ∑_{s ≤ M} 3^{−αs}, which is simultaneously ≤ M + 1 and ≤ Cgeo — that is exactly where the min comes from.

References

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

Elementary geometric facts

theorem Algsuperdiff.Probability.threePow_neg_natMul (t : ℝ) (j : ℕ) : 3 ^ (-(t * ↑j)) = (3 ^ (-t)) ^ j

Summability transfer between base points

The one-step layer recursion

The finite window induction (abstract in the layer tail T)

The rearrangement at an abstract ratio r ∈ (0,1)

The upward (Step-2) rearrangement

theorem Algsuperdiff.Probability.window_geom_tail_rearrange {α : ℝ} (hα : 0 < α) {Y : ℤ → ℝ} (hY : ∀ (l : ℤ), 0 ≤ Y l) {n m : ℤ} (hnm : n ≤ m) : ∑ k ∈ Finset.Icc n m, ∑' (j : ℕ), 3 ^ (-(α * ↑j)) * Y (k + ↑j) ≤ (1 - 3 ^ (-α))⁻¹ * ∑ l ∈ Finset.Icc n m, Y l + min (↑(m - n + 1)) (1 - 3 ^ (-α))⁻¹ * ∑' (j : ℕ), 3 ^ (-(α * ↑j)) * Y (m + 1 + ↑j)

The Step-2 window rearrangement (ABK26, l.minimal.scale.sep Step 2). For a nonnegative layer field Y : ℤ → ℝ and a geometric decay rate `α

0, ∑{k=n}^{m} ∑{l ≥ k} 3^{−α(l−k)} Y_l`

rearranges into a window sum with constant Cgeo = (1 − 3^{−α})⁻¹ plus a geometric tail beyond m with the sharper coefficient min(m − n + 1, Cgeo). No summability hypothesis: in the non-summable regime both sides degenerate to the tsum junk value.

theorem Algsuperdiff.Probability.window_geom_tail_rearrange_le {α : ℝ} (hα : 0 < α) {Y : ℤ → ℝ} (hY : ∀ (l : ℤ), 0 ≤ Y l) {n m : ℤ} (hnm : n ≤ m) : ∑ k ∈ Finset.Icc n m, ∑' (j : ℕ), 3 ^ (-(α * ↑j)) * Y (k + ↑j) ≤ (1 - 3 ^ (-α))⁻¹ * (∑ l ∈ Finset.Icc n m, Y l + ∑' (j : ℕ), 3 ^ (-(α * ↑j)) * Y (m + 1 + ↑j))

Crude corollary: the same rearrangement with the single constant Cgeo = (1 − 3^{−α})⁻¹ in front of both the window sum and the off-window tail. Weaker than window_geom_tail_rearrange (which sharpens the tail coefficient to min(m − n + 1, Cgeo)), but often the convenient shape.

The downward (Step-1) reflection

theorem Algsuperdiff.Probability.window_geom_head_rearrange {α : ℝ} (hα : 0 < α) {X : ℤ → ℝ} (hX : ∀ (l : ℤ), 0 ≤ X l) {n m : ℤ} (hnm : n ≤ m) : ∑ k ∈ Finset.Icc n m, ∑' (j : ℕ), 3 ^ (-(α * ↑j)) * X (k - ↑j) ≤ (1 - 3 ^ (-α))⁻¹ * ∑ l ∈ Finset.Icc n m, X l + min (↑(m - n + 1)) (1 - 3 ^ (-α))⁻¹ * ∑' (j : ℕ), 3 ^ (-(α * ↑j)) * X (n - 1 - ↑j)

The Step-1 window rearrangement. The reflection l ↦ −l of window_geom_tail_rearrange: a window sum of downward geometric layer tails splits into the window sum plus a head below n, with the sharp min coefficient on the head.