CutoffFrobeniusMassTail

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

Uniform tail of the per-cube cutoff Frobenius mass

This module specializes the translated stream-increment estimate to p = 2 and to the finite lower tail (m - (q + 1), m]. The elementary entrywise comparison between Frobenius and operator norms prices the finite per-cube mass by d^2 times that increment mass. The closed formula streamPointScale_sq then removes the lower endpoint from the amplitude, and the one-sided almost-everywhere limit theorem passes the same bound to the genuine cutoff.

Source and correction

• ABK26, e.kmn.bounds, label and display, gives the stream-increment estimate for every origin-cube scale l, assuming only n < m. The proved translation theorem carries that all-l statement to every translated triadic cube Q; this is the source authority for the arbitrary-Q theorem below.
• ABK26, records the finite-lower-cutoff passage and related increment estimates used by the specialization.
• ABK26, supplies the volume-normalized squared Frobenius expansion and estimates. Its restricted scale ranges support the Frobenius calculation but are not authority for the arbitrary-Q scope.

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

A dimension-only amplitude for finite and genuine cutoff Frobenius masses.

Equations

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

theorem Algsuperdiff.Section3.Provider.Stream.cutoffFrobeniusMassFiniteConst_pos (d : ℕ) : 0 < cutoffFrobeniusMassFiniteConst d

The dimension-only cutoff Frobenius-mass amplitude is strictly positive.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_one_finiteLowerCutoffFrobeniusMass {d : ℕ} (M : ABKModel d) (m : ℤ) (q : ℕ) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (fun (omega : Cutoff.CutoffSample d) => finiteLowerCutoffFrobeniusMass Q m (q + 1) omega) (cutoffFrobeniusMassFiniteConst d * M.gamma⁻¹ * 3 ^ (2 * (M.gamma * ↑m)))

Every finite lower cutoff has a uniform one-sided Gamma_1 per-cube Frobenius-mass tail at the dimension-only amplitude.

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