Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.Base.CutoffMassWeightedSum

CutoffMassWeightedSum #

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

Weighted aggregation of cutoff Frobenius-mass maxima #

This module performs the countable scalar aggregation needed by the corrected Section 3.2 base-case route. At descendant depth n, it weights the genuine cutoff Frobenius-mass maximum by the p = infinity, q = 2 Chapter 2 geometric weight and by nu^{-2}. The per-depth Gamma_1 estimates are combined with the countable generalized triangle inequality, while descendantMassFactor is summed into the adopted baseLoss d s.

source
noncomputable def Algsuperdiff.Section3.Provider.Base.cutoffMassLinearWeightedScale {d : ℕ} (M : ABKModel d) (m : ℤ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) :
ℝ

The scalar majorant for the linearly weighted cutoff-mass series.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Algsuperdiff.Section3.Provider.Base.cutoffMassLinearWeightedScale_pos {d : ℕ} (M : ABKModel d) (m : ℤ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) :
    0 < cutoffMassLinearWeightedScale M m s

    The weighted-series scalar majorant is strictly positive.

    source
    noncomputable def Algsuperdiff.Section3.Provider.Base.cutoffMassLinearWeightedSum {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (m : ℤ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) (omega : Cutoff.CutoffSample d) :
    ℝ

    The all-depth linearly weighted sum of genuine descendant cutoff-mass maxima.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algsuperdiff.Section3.Provider.Base.cutoffMassLinearWeightedSum_nonneg {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (m : ℤ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) (omega : Cutoff.CutoffSample d) :
      0 ≤ cutoffMassLinearWeightedSum M Q m s omega

      The all-depth linearly weighted cutoff-mass sum is nonnegative.

      source
      theorem Algsuperdiff.Section3.Provider.Base.isBigOWith_gammaSigma_one_cutoffMassLinearWeightedSum {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (m : ℤ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) :
      HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (cutoffMassLinearWeightedSum M Q m s) (HCPolySupport.IndependentSums.gammaTriangleConst 1 * cutoffMassLinearWeightedScale M m s)

      The linearly weighted all-depth cutoff mass has a one-sided Gamma_1 tail at the scalar baseLoss majorant.