MomentBoostedLargeEnvelope

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

Dimension-only envelope arithmetic for the sharp large-cube route

The finite-family transport leaves explicit numerical, color, and partition normalization factors. This module records the deterministic algebra showing how those factors fit the manuscript's single C(d) before the model and indices are quantified. It is internal support for the exact frozen export.

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

The number of available scale-zero colors, as a real dimension-only quantity.

Equations

• Algsuperdiff.Section3.Provider.Stream.momentBoostedColorEnvelope d = ↑(HCPolySupport.scaleColorPeriod 0) ^ ↑d

theorem Algsuperdiff.Section3.Provider.Stream.one_le_momentBoostedColorEnvelope (d : ℕ) : 1 ≤ momentBoostedColorEnvelope d

theorem Algsuperdiff.Section3.Provider.Stream.card_used_scaleZero_colors_le_momentBoostedColorEnvelope {d : ℕ} (j : ℤ) : ↑(Finset.image (HCPolySupport.cubeScaleColor 0) (HCPolySupport.descendantsAtScale (HCPolySupport.originCube d j) 0)).card ≤ momentBoostedColorEnvelope d

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

The fixed geometric loss incurred by shifting the partition down to scale zero.

Equations

• Algsuperdiff.Section3.Provider.Stream.momentBoostedPartitionShiftEnvelope d = 3 ^ (↑d * ↑(Algsuperdiff.Section3.Provider.Stream.incrementPartitionShift d))

theorem Algsuperdiff.Section3.Provider.Stream.one_le_momentBoostedPartitionShiftEnvelope (d : ℕ) : 1 ≤ momentBoostedPartitionShiftEnvelope d

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

The source-scale coefficient carried by streamPointScale.

Equations

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

theorem Algsuperdiff.Section3.Provider.Stream.momentBoostedStreamPointEnvelope_nonneg (d : ℕ) : 0 ≤ momentBoostedStreamPointEnvelope d

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

A single positive dimension-only envelope for the strict p > 2 branch. It is intentionally generous so the deterministic branch comparison remains transparent and no p-dependent concentration constant is hidden in it.

Equations

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

theorem Algsuperdiff.Section3.Provider.Stream.one_le_momentBoostedLargeCubeEnvelope (d : ℕ) : 1 ≤ momentBoostedLargeCubeEnvelope d

theorem Algsuperdiff.Section3.Provider.Stream.momentBoostedLargeCubeEnvelope_pos (d : ℕ) : 0 < momentBoostedLargeCubeEnvelope d

theorem Algsuperdiff.Section3.Provider.Stream.momentBoosted_sharp_scale_le_source_shape {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) (hp_two : 2 < p) {n m l : ℤ} (hnm : n < m) (hsl : m + ↑(incrementPartitionShift d) ≤ l) {q : ℝ} (hq : 1 ≤ q) (hqQ : q ≤ momentBoostedColorEnvelope d) : have sigma := 2 / p; have j := l - (m + ↑(incrementPartitionShift d)); 16 * q * q ^ (1 / sigma) * √(momentBoostedIndependentVariance sigma) * streamIncrementLpMomentBoostScale M p n m * HCPolySupport.Book.Ch04.partitionCardinalityScale 0 j ≤ (momentBoostedLargeCubeEnvelope d * p) ^ (p / 2) * (min M.gamma⁻¹ (↑m - ↑n) * 3 ^ (2 * M.gamma * ↑m)) ^ (p / 2) * 3 ^ (-(↑d / 2) * (↑l - ↑m))

theorem Algsuperdiff.Section3.Provider.Stream.momentBoosted_direct_scale_le_source_shape {d : ℕ} (M : ABKModel d) {p : ℝ} (hp : 1 ≤ p) (hp_two : 2 < p) {n m l : ℤ} (hnm : n < m) (hml : m ≤ l) (hwindow : ¬m + ↑(incrementPartitionShift d) ≤ l) : streamIncrementLpMomentBoostScale M p n m ≤ (momentBoostedLargeCubeEnvelope d * p) ^ (p / 2) * (min M.gamma⁻¹ (↑m - ↑n) * 3 ^ (2 * M.gamma * ↑m)) ^ (p / 2) * 3 ^ (-(↑d / 2) * (↑l - ↑m))