MomentBoostedLowPowerTransport

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

Stream transport for the low-power moment-boosted route

This module applies the deterministic two-regime colored Bernstein endpoint to the actual stream increment. The only comparison between exponents is the pointwise Jensen inequality on the cube: for 1 ≤ p ≤ 2, the p-mass is at most the p / 2 power of the two-mass. No such comparison is exposed as a new premise of a source-facing declaration.

theorem Algsuperdiff.Section3.Provider.Stream.streamIncrementLpMass_le_streamIncrementLpMass_two_rpow {d : ℕ} {p : ℝ} (hp : 0 < p) (hp_two : p ≤ 2) (l n m : ℤ) (omega : Cutoff.ShellSeq d) : streamIncrementLpMass p l n m omega ≤ streamIncrementLpMass 2 l n m omega ^ (p / 2)

The low-power cube-mass comparison used internally by the two-regime transport.

noncomputable def Algsuperdiff.Section3.Provider.Stream.normalizedLowPowerLpMassRep {d : ℕ} (P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d) (V : ℝ) (R : HCPolySupport.TriadicCube d) : HCPolySupport.RegCoeffField d → ℝ

The centered, scale-two partition summand normalized by its actual mass scale. It is internal data for the low-power coloring application.

Equations

• Algsuperdiff.Section3.Provider.Stream.normalizedLowPowerLpMassRep P V R = Algsuperdiff.Section3.Provider.Stream.normalizedCenteredLpMassRep P 2 V R

theorem Algsuperdiff.Section3.Provider.Stream.measurable_normalizedLowPowerLpMassRep {d : ℕ} (P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d) (V : ℝ) (R : HCPolySupport.TriadicCube d) : Measurable (normalizedLowPowerLpMassRep P V R)

theorem Algsuperdiff.Section3.Provider.Stream.local_normalizedLowPowerLpMassRep {d : ℕ} (P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d) (V : ℝ) (R : HCPolySupport.TriadicCube d) : HCPolySupport.Book.Ch04.IsRestrictionLocalRandomVariable (HCPolySupport.cubeSet R) ⋯ (normalizedLowPowerLpMassRep P V R)

theorem Algsuperdiff.Section3.Provider.Stream.map_normalizedLowPowerLpMassRep_descendant_eq_origin {d : ℕ} (M : ABKModel d) (V : ℝ) (n m j : ℤ) (hj : 0 ≤ j) (R : HCPolySupport.TriadicCube d) (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d j) 0) : MeasureTheory.Measure.map (normalizedLowPowerLpMassRep (partitionStreamIncrementLaw M n m) V R) (partitionStreamIncrementLaw M n m) = MeasureTheory.Measure.map (normalizedLowPowerLpMassRep (partitionStreamIncrementLaw M n m) V (HCPolySupport.originCube d 0)) (partitionStreamIncrementLaw M n m)

Stationarity makes every scale-zero descendant have the origin law for the normalized scale-two summand.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_streamIncrementLpMass_lowPower_partition {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) (hp_two : p ≤ 2) {n m l : ℤ} (hnm : n < m) (hsl : m + ↑(incrementPartitionShift d) ≤ l) : have K := streamIncrementLpMassScale M 2 n m; have j := l - (m + ↑(incrementPartitionShift d)); have S := HCPolySupport.descendantsAtScale (HCPolySupport.originCube d j) 0; have color := HCPolySupport.cubeScaleColor 0; HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma (2 / p)) (fun (omega : ℤ → Frozen.Assumptions.ShellField d) => streamIncrementLpMass p l n m omega - K ^ (p / 2)) (momentBoostedLowPowerColorConst ↑(Finset.image color S).card * K ^ (p / 2) / √↑S.card)

The low-power two-regime colored concentration bound, transported to the actual stream mass in the genuine large-partition regime.