MinkowskiScaleClosure

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

The Minkowski-ordered scale sum: the three per-scale shapes, closed

Everything below is abstract-real arithmetic: no model, no measure, no carrier occurs.

What is here

MinkowskiTransport.lean leaves the anchor's right-hand side as the single scalar

𝔠_{2s} ∑_{l ≥ 0} 3^{-sl} G_l ,

G_l the per-cube L^{p/2} moment at the descendant scale n − l. The proved per-cube moment layer produces G_l in exactly three shapes:

• a uniform part K p γ s^{-2} (Step 3's first and third summands: their majorants do not see the descendant scale -- this is why the manuscript calls them straightforward);
• a linear-times-exponential part K p γ (m−j) 3^{2γ(m−j)} (Step 3's second summand at the value slot, m − j = (m−n)+l); and
• a flat exponential part K p γ 3^{2γ(m−j)} (the additive 1 in the value bullet, and the deterministic σ ratio leg).

This module evaluates all three against the geometric weight, in the ℓ¹ ordering:

𝔠_{2s} ∑_l 3^{-sl} · γ A                     ≤ 2 γ A                (uniform)
𝔠_{2s} ∑_l 3^{-sl} · γ(D+l) 3^{2γ(D+l)}      ≤ γ(36 D + 144/s)      (ScaleSumOrdering)
𝔠_{2s} ∑_l 3^{-sl} · γ 3^{2γ(D+l)}           ≤ 36 γ/s               (flat)

References

• ABK26, l.bounds.mathcal.E.aL, Step 5.

1. The geometric ratio and the termwise domination

theorem Algsuperdiff.Section4.Provider.BoundsEaL.tsum_rpow_three_neg_mul_nat {s : ℝ} (hs : 0 < s) : ∑' (l : ℕ), 3 ^ (-(s * ↑l)) = (1 - 3 ^ (-s))⁻¹

∑_{l ≥ 0} 3^{-sl} = (1 - 3^{-s})^{-1}.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.geometricTwo_mul_tsum_le_two {s : ℝ} (hs : 0 < s) : (1 - 3 ^ (-(2 * s))) * ∑' (l : ℕ), 3 ^ (-(s * ↑l)) ≤ 2

The uniform shape. 𝔠_{2s} ∑_l 3^{-sl} ≤ 2, the exact cancellation 𝔠_{2s}/𝔠_s = 1 + 3^{-s} ≤ 2.

2. The three shapes

theorem Algsuperdiff.Section4.Provider.BoundsEaL.summable_flatScaleTerm {s gam D : ℝ} (hs : 0 < s) (hgam : 0 ≤ gam) (h4gam : 4 * gam ≤ s) (hgamD : gam * D ≤ 1) : Summable fun (l : ℕ) => 3 ^ (-(s * ↑l)) * (gam * 3 ^ (2 * gam * (D + ↑l)))

Summability of the flat shape.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.flatScaleSum_le {s gam D : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (hgam : 0 ≤ gam) (h4gam : 4 * gam ≤ s) (hgamD : gam * D ≤ 1) : (1 - 3 ^ (-(2 * s))) * ∑' (l : ℕ), 3 ^ (-(s * ↑l)) * (gam * 3 ^ (2 * gam * (D + ↑l))) ≤ gam * (36 / s)

The flat shape. 𝔠_{2s} ∑_l 3^{-sl} γ 3^{2γ(D+l)} ≤ 36 γ/s.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.summable_linearScaleTerm {s gam D : ℝ} (hs : 0 < s) (hgam : 0 ≤ gam) (h4gam : 4 * gam ≤ s) (hD : 0 ≤ D) (hgamD : gam * D ≤ 1) : Summable fun (l : ℕ) => 3 ^ (-(s * ↑l)) * (gam * (D + ↑l) * 3 ^ (2 * gam * (D + ↑l)))

Summability of the linear-times-exponential shape (the shape ScaleSumOrdering.minkowskiOrder_scaleSum_le evaluates). A local re-derivation of that proof's internal hsumLHS.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.summable_constScaleTerm {s c : ℝ} (hs : 0 < s) : Summable fun (l : ℕ) => 3 ^ (-(s * ↑l)) * c

Summability of the uniform shape.

3. The three shapes, summed

theorem Algsuperdiff.Section4.Provider.BoundsEaL.minkowskiScaleSum_total_le {s gam D A : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (hgam : 0 ≤ gam) (h4gam : 4 * gam ≤ s) (hD : 0 ≤ D) (hgamD : gam * D ≤ 1) (hA : 0 ≤ A) : (1 - 3 ^ (-(2 * s))) * ∑' (l : ℕ), 3 ^ (-(s * ↑l)) * (gam * A + (gam * (D + ↑l) * 3 ^ (2 * gam * (D + ↑l)) + gam * 3 ^ (2 * gam * (D + ↑l)))) ≤ gam * (2 * A + 36 * D + 180 / s)

The Minkowski-ordered scale sum, closed.

For 0 < s ≤ 1, 4γ ≤ s, 0 ≤ D with γD ≤ 1 (the anchor's own binder m ≤ n + γ^{-1}) and 0 ≤ A,

𝔠_{2s} ∑_{l ≥ 0} 3^{-sl} · ( γA + γ(D+l)3^{2γ(D+l)} + γ 3^{2γ(D+l)} )
    ≤ γ (2A + 36D + 180/s) .

The three summands are exactly the three shapes the proved per-cube moment layer produces.

4. The square root, against the anchor's own scalar

theorem Algsuperdiff.Section4.Provider.BoundsEaL.sqrt_minkowskiScaleSum_le {s gam D : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (hgam : 0 ≤ gam) (hD : 0 ≤ D) : √(gam * (2 * (s⁻¹ * s⁻¹) + 36 * D + 180 / s)) ≤ 16 * √gam * (s⁻¹ + √D)

The square root, at the anchor's own scalar.

With the uniform slot at A = s^{-2},

√( γ (2 s^{-2} + 36 D + 180/s) )  ≤  16 √γ ( s^{-1} + √D ) ,