CutoffCoarseNormBounds

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

Coarse-matrix norm bounds for the coefficient cutoff

This module turns the specialized cutoff Loewner chain into operator-norm bounds on every triadic cube. The upper coarse matrix is controlled by the volume-normalized squared Frobenius mass of the stream, while the inverse starred matrix is controlled deterministically by nu⁻¹. Finite suprema give the corresponding bounds over every fixed descendant depth.

The proof on an arbitrary cube is reduced to the centered cube of the same scale. BadEvents.coarseBlockMatrix_cutoff_translateCutoffSample supplies the coarse-block covariance directly. Translation invariance of normalized volume averages identifies the centered Frobenius mass with the mass on the original cube. Thus no root-cube supremum replaces a translated local mass.

Main results

• coarseBMatrixNorm_coefficientCutoff_le bounds the upper coarse-matrix norm on an arbitrary cube by nu + nu⁻¹ times its cutoff Frobenius mass.
• coarseSigmaStarInvMatrixNorm_coefficientCutoff_le bounds the inverse starred coarse-matrix norm by nu⁻¹.
• maxDescendantBMatrixNormAtScale_coefficientCutoff_le and maxDescendantSigmaStarInvMatrixNormAtScale_coefficientCutoff_le give the corresponding fixed-depth descendant bounds.

theorem Algsuperdiff.Section3.Provider.Base.coarseBMatrixNorm_coefficientCutoff_le {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (m : ℤ) (omega : Cutoff.CutoffSample d) : HCPolySupport.Book.Ch02.coarseBMatrixNorm Q (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega) ≤ M.nu + M.nu⁻¹ * Stream.cutoffFrobeniusMass Q m omega

On every triadic cube, the upper coarse-matrix norm of the cutoff is at most nu + nu⁻¹ times the local squared Frobenius mass.

theorem Algsuperdiff.Section3.Provider.Base.coarseSigmaStarInvMatrixNorm_coefficientCutoff_le {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (m : ℤ) (omega : Cutoff.CutoffSample d) : HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm Q (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega) ≤ M.nu⁻¹

On every triadic cube, the inverse starred coarse-matrix norm of the coefficient cutoff is at most nu⁻¹.

theorem Algsuperdiff.Section3.Provider.Base.maxDescendantBMatrixNormAtScale_coefficientCutoff_le {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (m : ℤ) (n : ℕ) (omega : Cutoff.CutoffSample d) : HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale Q (Q.scale - ↑n) (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega) ≤ M.nu + M.nu⁻¹ * Stream.cutoffFrobeniusMassMaximum Q m n omega

At a fixed descendant depth, the maximal upper coarse-matrix norm is controlled by the genuine maximum of the translated local Frobenius masses.

theorem Algsuperdiff.Section3.Provider.Base.maxDescendantSigmaStarInvMatrixNormAtScale_coefficientCutoff_le {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (m : ℤ) (n : ℕ) (omega : Cutoff.CutoffSample d) : HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega) ≤ M.nu⁻¹

At every fixed descendant depth, the maximal inverse starred coarse-matrix norm of the coefficient cutoff is at most nu⁻¹.