CutoffFrobeniusMassMaximum

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

Descendant maxima of the genuine cutoff Frobenius mass

This module takes the genuine per-cube cutoff mass delivered by CutoffFrobeniusMassTail and forms its literal finite maximum over descendantsAtDepth Q n. The family is canonically nonempty, so Finset.sup' is used without an empty-family convention. Every member is bounded by that maximum, and the maximum remains measurable and nonnegative.

For the tail estimate, depth zero is handled as the singleton {Q}, retaining the exact factor 1. At positive depth the model supplies 2 ≤ d, the family has cardinality (3 ^ d) ^ n, and the finite-maximum Gamma_1 theorem costs exactly 3 d log(3) n, the positive-depth branch of descendantMassFactor d n.

Source

• ABK26 e.kmn.bounds, label and display, supplies the uniform one-cube increment tail used by the genuine per-cube provider.
• ABK26 l.maximums.Gamma.s, supplies the finite-maximum Gamma_sigma step and its logarithmic cardinality cost.
• This file provides precisely the genuine finite-depth mass maximum; it does not claim the later weighted all-depth aggregation.

noncomputable def Algsuperdiff.Section3.Provider.Stream.cutoffFrobeniusMassMaximum {d : ℕ} (Q : HCPolySupport.TriadicCube d) (m : ℤ) (n : ℕ) (omega : Cutoff.CutoffSample d) : ℝ

The genuine maximum of the cutoff Frobenius mass over all depth-n descendants of Q.

Equations

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

theorem Algsuperdiff.Section3.Provider.Stream.cutoffFrobeniusMassMaximum_nonneg {d : ℕ} (Q : HCPolySupport.TriadicCube d) (m : ℤ) (n : ℕ) (omega : Cutoff.CutoffSample d) : 0 ≤ cutoffFrobeniusMassMaximum Q m n omega

A descendant cutoff Frobenius-mass maximum is nonnegative.

theorem Algsuperdiff.Section3.Provider.Stream.measurable_cutoffFrobeniusMassMaximum {d : ℕ} (Q : HCPolySupport.TriadicCube d) (m : ℤ) (n : ℕ) : Measurable (cutoffFrobeniusMassMaximum Q m n)

The descendant cutoff Frobenius-mass maximum is measurable on the public cutoff carrier.

theorem Algsuperdiff.Section3.Provider.Stream.cutoffFrobeniusMass_le_cutoffFrobeniusMassMaximum {d : ℕ} (Q : HCPolySupport.TriadicCube d) (m : ℤ) (n : ℕ) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtDepth Q n) (omega : Cutoff.CutoffSample d) : cutoffFrobeniusMass R m omega ≤ cutoffFrobeniusMassMaximum Q m n omega

Every member of the descendant family is bounded by its genuine maximum.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_one_cutoffFrobeniusMassMaximum {d : ℕ} (M : ABKModel d) (m : ℤ) (n : ℕ) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (cutoffFrobeniusMassMaximum Q m n) (cutoffFrobeniusMassFiniteConst d * Scales.descendantMassFactor d n * M.gamma⁻¹ * 3 ^ (2 * (M.gamma * ↑m)))

The genuine depth-n descendant maximum has the exact dimension-depth Gamma_1 amplitude obtained from the one-cube tail and finite maxima.