P4Bounds

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

Samplewise coarse-ellipticity bounds for the genuine cutoff

The actual cutoff has deterministic lower coercivity nu, but its upper ellipticity is a local random envelope. This module records the exact bridge from that envelope to CoarseGraining's Chapter 4 upper coarse observable. It does not replace the random upper envelope by nu or assert (P4) prematurely.

theorem Algsuperdiff.Section3.Cutoff.coefficientCutoff_aelocallyUniformlyElliptic {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField (coefficientCutoff M.nu m omega)

The Chapter 4 field is locally a.e.-elliptic on every genuine cutoff sample, with the cube-wise sample-dependent upper envelope from CoefficientFamily.

theorem Algsuperdiff.Section3.Cutoff.coefficientCutoff_canonicalFamily_aeeq {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) : (HCPolySupport.Book.Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField (coefficientCutoff M.nu m omega) ⋯).AEEq (coefficientCutoffTriadicCoeffFamily M m omega)

The canonical CoarseGraining coefficient family and the literal cutoff family have the same representatives on every cube.

theorem Algsuperdiff.Section3.Cutoff.maxDescendantBMatrixNormAtScale_le_cutoffEnvelope {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) (Q : HCPolySupport.TriadicCube d) (n : ℕ) : HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale Q (Q.scale - ↑n) (coefficientCutoffTriadicCoeffFamily M m omega) ≤ 4 * ↑d * M.nu⁻¹ * coefficientCutoffCubeEllipticityUpper M m omega Q ^ 2

A descendant upper-block maximum is controlled by the upper ellipticity envelope of its root cube. The envelope is the genuine random one.

theorem Algsuperdiff.Section3.Cutoff.maxDescendantBMatrixNormCoeffFieldAtScale_le_cutoffEnvelope {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) (Q : HCPolySupport.TriadicCube d) (n : ℕ) : HCPolySupport.Book.Ch04.maxDescendantBMatrixNormCoeffFieldAtScale Q (Q.scale - ↑n) (coefficientCutoff M.nu m omega) ≤ 4 * ↑d * M.nu⁻¹ * coefficientCutoffCubeEllipticityUpper M m omega Q ^ 2

The ambient Chapter 4 descendant observable agrees with the literal cutoff family, and hence inherits the same root-cube envelope bound.

theorem Algsuperdiff.Section3.Cutoff.maxDescendantSigmaStarInvMatrixNormAtScale_le_cutoffCoercivity {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) (Q : HCPolySupport.TriadicCube d) (n : ℕ) : HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) (coefficientCutoffTriadicCoeffFamily M m omega) ≤ 4 * ↑d * M.nu⁻¹

The lower inverse descendant maximum uses only the literal coercivity nu; the sample-dependent upper envelope plays no role in this bound.

theorem Algsuperdiff.Section3.Cutoff.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale_le_cutoffCoercivity {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) (Q : HCPolySupport.TriadicCube d) (n : ℕ) : HCPolySupport.Book.Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale Q (Q.scale - ↑n) (coefficientCutoff M.nu m omega) ≤ 4 * ↑d * M.nu⁻¹

Ambient Chapter 4 form of the deterministic lower inverse descendant bound.

theorem Algsuperdiff.Section3.Cutoff.LambdaSqCoeffField_le_cutoffEnvelope {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) (Q : HCPolySupport.TriadicCube d) {s : ℝ} (hs : 0 < s) : HCPolySupport.Book.Ch04.LambdaSqCoeffField Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 1) (coefficientCutoff M.nu m omega) ≤ 4 * ↑d * M.nu⁻¹ * coefficientCutoffCubeEllipticityUpper M m omega Q ^ 2

Exact samplewise upper bound for CoarseGraining's Λ_{s,1} observable. This is the bridge that permits the Γ₂ moments of the local cutoff control to feed the upper (P4) moment; it retains the random local upper constant.

theorem Algsuperdiff.Section3.Cutoff.lambdaSqCoeffField_inv_le_cutoffCoercivity {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) (Q : HCPolySupport.TriadicCube d) {s : ℝ} (hs : 0 < s) : (HCPolySupport.Book.Ch04.lambdaSqCoeffField Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 1) (coefficientCutoff M.nu m omega))⁻¹ ≤ 4 * ↑d * M.nu⁻¹

Exact samplewise lower (P4) bound: the inverse lower coarse observable is uniformly controlled by the molecular coercivity nu.