DescendantMassFactor

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

Descendant-mass aggregation for the corrected Section 3.2 base case

At descendant depth n, the retained per-cube mass envelope contributes the factor 1 + 3 d log(3) n. The normalized q = 2 geometric weights have first moment at most 2 / s, so the weighted factor is bounded by `baseLoss d s = 1

• 6 d log(3) / s`.

The mathematical source role is confined to the scalar aggregation behind ABK26 Proposition p.base.case, display e.basecase.mathcal.E at label and its derivation. In particular, this file does not assert the false global-root-supremum step.

noncomputable def Algsuperdiff.Section3.Provider.Scales.descendantMassFactor (d n : ℕ) : ℝ

The linear loss factor contributed by descendants at depth n.

Equations

• Algsuperdiff.Section3.Provider.Scales.descendantMassFactor d n = 1 + 3 * ↑d * Real.log 3 * ↑n

theorem Algsuperdiff.Section3.Provider.Scales.descendantMassFactor_pos (d n : ℕ) : 0 < descendantMassFactor d n

The descendant-mass factor is strictly positive.

noncomputable def Algsuperdiff.Section3.Provider.Scales.geometricRatio (s : ℝ) : ℝ

The common ratio 3 ^ (-2s) of the q = 2 scale weights.

Equations

• Algsuperdiff.Section3.Provider.Scales.geometricRatio s = Real.rpow 3 (-s * 2)

theorem Algsuperdiff.Section3.Provider.Scales.summable_geometricWeight_mul_descendantMassFactor (d : ℕ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) : Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight (↑s) 2 n * descendantMassFactor d n

The normalized q = 2 geometric weights make the descendant-mass factors summable.

theorem Algsuperdiff.Section3.Provider.Scales.tsum_geometricWeight_mul_descendantMassFactor_eq (d : ℕ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) : ∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight (↑s) 2 n * descendantMassFactor d n = 1 + 3 * ↑d * Real.log 3 * (Real.rpow 3 (-↑s * 2) / (1 - Real.rpow 3 (-↑s * 2)))

Exact collapse of the weighted descendant-mass factors through the first moment.

theorem Algsuperdiff.Section3.Provider.Scales.tsum_geometricWeight_mul_descendantMassFactor_le_baseLoss (d : ℕ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) : ∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight (↑s) 2 n * descendantMassFactor d n ≤ baseLoss d s

The exact weighted factor is bounded by the adopted Option-A base loss.