MomentBoostedLargeTransport

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

Stream-specific transport for the sharp moment-boosted large-cube route

This module begins the application of the internal moment-boosted finite-family endpoint to the actual partition-normalized stream increment. It rederives the stationarity transport for the centered local representative using only public clean A. In particular, no frozen declaration and no generic Gamma_sigma coloring theorem is used.

The eventual public source theorem is assembled in a later focused provider; the declarations here remain internal proof architecture.

Measurability needed by the final one-sided wrapper

theorem Algsuperdiff.Section3.Provider.Stream.measurable_streamIncrementLpMass_for_momentBoosted {d : ℕ} {p : ℝ} (hp : 0 < p) (l n m : ℤ) : Measurable (streamIncrementLpMass p l n m)

Law transport for one-sided tails

The actual centered local variable

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_normalizedCenteredLpMassRep_origin_momentBoosted {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) : have P := partitionStreamIncrementLaw M n m; have V := streamIncrementLpMomentBoostScale M p n m; HCPolySupport.IndependentSums.IsBigOWith P (momentBoostedGammaSigma (2 / p)) (normalizedCenteredLpMassRep P p V (HCPolySupport.originCube d 0)) 1

The normalized origin summand has unit strengthened one-sided control. The scale is the actual all-real moment scale from IncrementLp.lean, not a generic weak-Orlicz conversion constant.

theorem Algsuperdiff.Section3.Provider.Stream.normalizedCenteredLpMassRep_origin_moments {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) {n m : ℤ} (hnm : n < m) : have P := partitionStreamIncrementLaw M n m; have V := streamIncrementLpMomentBoostScale M p n m; have Y := normalizedCenteredLpMassRep P p V (HCPolySupport.originCube d 0); MeasureTheory.Integrable Y P ∧ MeasureTheory.Integrable (fun (a : HCPolySupport.RegCoeffField d) => |Y a| ^ 2) P ∧ ∫ (a : HCPolySupport.RegCoeffField d), Y a ∂P = 0 ∧ ∫ (a : HCPolySupport.RegCoeffField d), |Y a| ^ 2 ∂P ≤ 1

The same normalized origin summand is centered, integrable, and has a unit second-moment proxy. This consumes the genuine variance estimate from the moment-growth proof; it does not assume a second-moment premise.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_streamIncrementLpMass_sub_originMean_momentBoosted {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) (hp_two : 2 < p) {n m l : ℤ} (hnm : n < m) (hsl : m + ↑(incrementPartitionShift d) ≤ l) : have sigma := 2 / p; have V := streamIncrementLpMomentBoostScale M p n m; have j := l - (m + ↑(incrementPartitionShift d)); HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma sigma) (fun (omega : Cutoff.ShellSeq d) => streamIncrementLpMass p l n m omega - ∫ (w : ℤ → Frozen.Assumptions.ShellField d), streamIncrementLpMass p (m + ↑(incrementPartitionShift d)) n m w ∂↑M.P) (16 * ↑(Finset.image (HCPolySupport.cubeScaleColor 0) (HCPolySupport.descendantsAtScale (HCPolySupport.originCube d j) 0)).card * ↑(Finset.image (HCPolySupport.cubeScaleColor 0) (HCPolySupport.descendantsAtScale (HCPolySupport.originCube d j) 0)).card ^ (1 / sigma) * √(momentBoostedIndependentVariance sigma) * V * HCPolySupport.Book.Ch04.partitionCardinalityScale 0 j)

The sharp centered-average estimate transported back to the shell-sequence law. It is still an internal large-partition lemma; the deterministic head and the final dimension-only envelope are assembled separately.