CutoffResponseMass

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

Cutoff response bound by the annealed plateau and descendant mass

This module proves the deterministic response bridge needed by the corrected Section 3.2 base-case route. The named normalized-response estimate bounds each descendant response by the two coarse matrix norms. The sharp cutoff coarse-norm bounds then leave a deterministic annealed plateau amplitude and the genuine squared Frobenius mass on that descendant. CoarseGraining's literal p = infinity, q = 2 series identity aggregates these estimates without replacing translated descendant masses by a root-cube supremum.

noncomputable def Algsuperdiff.Section3.Provider.Base.cutoffPlateauAmplitude {d : ℕ} (M : ABKModel d) (m : ℤ) : ℝ

The deterministic plateau amplitude in e.plateau.region.bound.

Equations

• Algsuperdiff.Section3.Provider.Base.cutoffPlateauAmplitude M m = Algsuperdiff.Section3.Disorder.cstarPlus M * (2 * M.nu ^ 2)⁻¹ * M.gamma⁻¹ * (1 + 4 * M.gamma) * 3 ^ (2 * M.gamma * ↑m)

theorem Algsuperdiff.Section3.Provider.Base.cutoffPlateauAmplitude_pos {d : ℕ} (M : ABKModel d) (m : ℤ) : 0 < cutoffPlateauAmplitude M m

The deterministic cutoff plateau amplitude is strictly positive.

theorem Algsuperdiff.Section3.Provider.Base.sigmaBar_weighted_plateau_le_cutoffPlateauAmplitude {d : ℕ} (M : ABKModel d) (m : ℤ) : (↑(Annealed.sigmaBar M m))⁻¹ * M.nu + ↑(Annealed.sigmaBar M m) * M.nu⁻¹ - 2 ≤ cutoffPlateauAmplitude M m

The scalar mismatch between the annealed comparator and nu is bounded by the deterministic plateau amplitude.

theorem Algsuperdiff.Section3.Provider.Base.maxDescendantNormalizedBlockResponseAtScale_coefficientCutoff_le {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (m : ℤ) (n : ℕ) (omega : Cutoff.CutoffSample d) : HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale Q (Q.scale - ↑n) (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega) (HCPolySupport.scalarMatrix ↑(Annealed.sigmaBar M m)) ≤ cutoffPlateauAmplitude M m + M.nu⁻¹ ^ 2 * Stream.cutoffFrobeniusMassMaximum Q m n omega

At every descendant depth, the normalized cutoff response is bounded by the deterministic plateau amplitude plus the genuine descendant mass maximum.

theorem Algsuperdiff.Section3.Provider.Base.homogenizationErrorOnCube_coefficientCutoff_sq_le {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (m : ℤ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) (omega : Cutoff.CutoffSample d) : HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q (↑s) HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega) (HCPolySupport.scalarMatrix ↑(Annealed.sigmaBar M m)) ^ 2 ≤ cutoffPlateauAmplitude M m + cutoffMassLinearWeightedSum M Q m s omega

On every cube and sample, the squared literal p = infinity, q = 2 cutoff homogenization error is bounded by the plateau and weighted mass sum.

theorem Algsuperdiff.Section3.Provider.Base.ae_cutoffHomogenizationError_sq_le_cutoffPlateauAmplitude_add_mass {d : ℕ} (M : ABKModel d) (m : ℤ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), Observable.cutoffHomogenizationError M m ⟨↑s, ⋯⟩ omega ^ 2 ≤ cutoffPlateauAmplitude M m + cutoffMassLinearWeightedSum M (HCPolySupport.originCube d m) m s omega

The public measurable cutoff error satisfies the plateau-plus-mass bound almost everywhere under the genuine cutoff-sample law.