MinkowskiTransport

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

The q = 2 scale sum, transported at the MINKOWSKI ordering

Why this module exists

AeMeasurableTransport/Step5PerCube/WeightedScaleClosure transport the anchor's left-hand side through Step 1's Jensen ordering: the geometric scale weight sits INSIDE the p-th power, so after the p-th root it acts at the rate s/p.

𝓔(ω) = ( ∑_{l ≥ 0} 𝔠_{2s} 3^{-2sl} · max_{R ∈ desc(□_m, n-l)} J(R; ã_{L,m}) )^{1/2}

(Support.fluxCorrectedTwoScaleErrorFunctional, literally) presents the scale sum OUTSIDE the p-th power, so the per-scale L^{p/2} moments combine by MINKOWSKI in L^{p/2} (MinkowskiLp.lean), not by Jensen.

This module performs that transport, and only that:

E[ (sup_{L ≥ m} 𝓔)^p ]  ≤  ( 3^{½ s(m-n)} )^p · ( ∑'_l 𝔠_{2s} 3^{-sl} G_l )^{p/2} ,

where G_l is any per-cube p/2-moment majorant at the descendant scale n − l. Three ingredients:

1. the a.e. L-free majorization of the carrier's per-scale slots (the proved MajorantTransport split, read through the carrier's own representative identification, so that the sup_L passes INSIDE the weighted sum);
2. countable Minkowski in L^{p/2} (MinkowskiLp.lean);
3. the descendant-count conversion at the norm level: max_R ≤ (∑_R (·)^{p/2})^{2/p} costs (3^{d(m-n+l)})^{2/p} ≤ 3^{s(m-n+l)}, which is exactly the anchor's own floor p ≥ 2ds^{-1}. The geometric weight 3^{-2sl} absorbs the 3^{sl} and leaves 3^{-sl}; the residual 3^{s(m-n)} becomes the printed prefactor 3^{½ s(m-n)} after the square root.

No γ-power, no s-power and no p-range is moved: the only inequality on parameters used below is the anchor's floor p ≥ 2ds^{-1}.

References

• ABK26, l.bounds.mathcal.E.aL, Step 1, Step 2, Step 5; d.mathcal.E.

1. Four elementary helpers

theorem Algsuperdiff.Section4.Provider.BoundsEaL.card_descendantsAtScale_originCube_eq_rpow (d : ℕ) {m k : ℤ} (hk : k ≤ m) : ↑(HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) k).card = Real.rpow 3 (↑d * (↑m - ↑k))

The descendant count, as a real power of three: #desc(□_m, k) = 3^{d(m−k)} for k ≤ m. This is the object the anchor's floor p ≥ 2ds^{-1} prices.

2. The transport, at an abstract per-cube majorant

3. The transport at the L-free majorant

theorem Algsuperdiff.Section4.Provider.BoundsEaL.lintegral_observableSup_rpow_le_minkowskiScaleSum (d : ℕ) (dimension : 2 ≤ d) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d) (m n : ℤ), n ≤ m → ∀ (s : { s : ℝ // 0 < s }), ↑s ≤ 1 / 4 → M.gamma ≤ 1 / 8 → ∀ (p : ℝ), 2 * ↑d * (↑s)⁻¹ ≤ p → ∀ (G : ℕ → ℝ), (∀ (l : ℕ), 0 ≤ G l) → (∀ (l : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (n - ↑l), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (lFreeStep3Majorant C M m (↑s) (lFreeGradSlot m (tailSeriesGauge m)) (lFreeValueSlot m (tailSeriesGauge m)) R omega) ^ (p / 2) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (G l) ^ (p / 2)) → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.fluxCorrectedTwoScaleErrorObservableSup M m n s omega ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (Real.rpow 3 (1 / 2 * ↑s * (↑m - ↑n))) ^ p * (∑' (l : ℕ), ENNReal.ofReal (HCPolySupport.Book.Ch02.geometricDiscount (↑s) 2 * (Real.rpow 3 (-↑s * ↑l) * G l))) ^ (p / 2)

The anchor's left-hand side at the Minkowski ordering.

If at every scale n − l and every descendant cube R of □_m at that scale the p/2-th moment of the L-free Step-3 majorant is at most (ofReal (G l))^{p/2}, then

E[ (sup_{L ≥ m} 𝓔_{s,∞,2}(□_m, n))^p ]
    ≤ (3^{½ s(m−n)})^p · ( ∑'_l 𝔠_{2s} · 3^{−sl} · G_l )^{p/2} .

The printed prefactor 3^{½ s(m−n)} comes out, and no constraint on p beyond the anchor's own floor p ≥ 2ds^{-1} is used.

The per-cube hypothesis is a conditional API obligation: it is Step 5's inner (Hölder) half, which this module does not prove.