MomentBoostedLowPowerProvider

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

Low-power assembly for the moment-boosted large-cube route

This module turns the deterministic two-regime low-power concentration result into the source-scale one-sided tail used by the final all-p provider. It keeps the 1 ≤ p ≤ 2 Jensen/Bernstein argument internal: no low-power comparison, partition condition, or moment statement becomes a premise of a source-facing declaration.

noncomputable def Algsuperdiff.Section3.Provider.Stream.momentBoostedLowPowerEnvelope (d : ℕ) : ℝ

Dimension-only envelope for the 1 ≤ p ≤ 2 branch. Squaring the fixed color and partition losses is exactly what permits their absorption through the concave exponent p / 2 ≥ 1 / 2.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Stream.one_le_momentBoostedLowPowerEnvelope (d : ℕ) : 1 ≤ momentBoostedLowPowerEnvelope d

theorem Algsuperdiff.Section3.Provider.Stream.momentBoostedLowPowerEnvelope_pos (d : ℕ) : 0 < momentBoostedLowPowerEnvelope d

theorem Algsuperdiff.Section3.Provider.Stream.isDeterministicShiftOneSidedOrlicz_streamIncrementLpMass_lowPower_partition_raw {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; Probability.IsDeterministicShiftOneSidedOrlicz (↑M.P) (HCPolySupport.IndependentSums.gammaSigma (2 / p)) (streamIncrementLpMass p l n m) (K ^ (p / 2)) (momentBoostedLowPowerColorConst ↑(Finset.image color S).card * K ^ (p / 2) / √↑S.card)

The low-power colored endpoint in one-sided wrapper form before its dimension-only source-scale envelope is applied.

noncomputable def Algsuperdiff.Section3.Provider.Stream.momentBoostedLowPowerTargetScale {d : ℕ} (M : ABKModel d) (p : ℝ) (l n m : ℤ) : ℝ

The source-shaped scale used to absorb the deterministic low-power branch. It is parameterized only by the model and indices; its constant is fixed by the ambient dimension before any model is chosen.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Stream.isDeterministicShiftOneSidedOrlicz_streamIncrementLpMass_lowPower_partition_envelope {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) (hp_two : p ≤ 2) {n m l : ℤ} (hnm : n < m) (hsl : m + ↑(incrementPartitionShift d) ≤ l) : Probability.IsDeterministicShiftOneSidedOrlicz (↑M.P) (HCPolySupport.IndependentSums.gammaSigma (2 / p)) (streamIncrementLpMass p l n m) ((momentBoostedLowPowerEnvelope d * p) ^ (p / 2) * (min M.gamma⁻¹ (↑m - ↑n) * 3 ^ (2 * M.gamma * ↑m)) ^ (p / 2)) (momentBoostedLowPowerTargetScale M p l n m)

The 1 ≤ p ≤ 2 partition carrier after both the deterministic shift and tail have been enlarged to the fixed dimension-only low-power envelope. The exponent split and partition condition are internal case-split data.