CutoffHomogenizationError

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

The cutoff homogenization error

This file exposes the measurable Section 3 observable \mathcal E_{s,\infty,2}(\square_m; a_m, \bar\sigma_r\operatorname{Id}) on its source domain 0 < s. The auxiliary comparator scale r remains explicit; the paper's state variable is the specialization r = m.

The public definitions use the genuine coefficient cutoff, genuine running diffusivity, and the verified measurable representative. Their almost-everywhere characterizations retain the separate coefficient, domain, and comparator scale roles and identify the observable with CoarseGraining's literal homogenization error.

Main definitions

• cutoffHomogenizationErrorAtComparatorScale: coefficient and cube scale m, with running-diffusivity comparator taken at a separately specified scale.
• cutoffHomogenizationError: the manuscript specialization whose three scales are all m.

References

• ABK26, definition d.mathcal.E, (2.28).
• ABK26, definition d.mathcalS.def, Section 3.1.

theorem Algsuperdiff.Section3.Observable.neZero_of_model_CutoffHomogenizationError {d : ℕ} (M : ABKModel d) : NeZero d

The paper-wide assumption 2 ≤ d, stored in the model, supplies the nonzero-dimension instance required by CoarseGraining's doubled-response A.

noncomputable def Algsuperdiff.Section3.Observable.cutoffHomogenizationErrorAtComparatorScale {d : ℕ} (M : ABKModel d) (m comparatorScale : ℤ) (s : { s : ℝ // 0 < s }) : Cutoff.CutoffSample d → ℝ

The measurable cutoff homogenization error with coefficient and cube scale m and running-diffusivity comparator taken at comparatorScale: \mathcal E_{s,\infty,2}(\square_m; a_m, \bar\sigma_{\mathit{comparatorScale}}\operatorname{Id}).

Equations

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

noncomputable def Algsuperdiff.Section3.Observable.cutoffHomogenizationError {d : ℕ} (M : ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) : Cutoff.CutoffSample d → ℝ

The actual Section 3 homogenization error \mathcal E_{s,\infty,2}(\square_m; a_m, \bar\sigma_m\operatorname{Id}).

Equations

• Algsuperdiff.Section3.Observable.cutoffHomogenizationError M m s = Algsuperdiff.Section3.Observable.cutoffHomogenizationErrorAtComparatorScale M m m s

theorem Algsuperdiff.Section3.Observable.measurable_cutoffHomogenizationErrorAtComparatorScale {d : ℕ} (M : ABKModel d) (m comparatorScale : ℤ) (s : { s : ℝ // 0 < s }) : Measurable (cutoffHomogenizationErrorAtComparatorScale M m comparatorScale s)

The cutoff homogenization error with a separate comparator scale is measurable under the genuine cutoff-sample law.

theorem Algsuperdiff.Section3.Observable.measurable_cutoffHomogenizationError {d : ℕ} (M : ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) : Measurable (cutoffHomogenizationError M m s)

The actual Section 3 cutoff homogenization error is measurable.

theorem Algsuperdiff.Section3.Observable.cutoffHomogenizationErrorAtComparatorScale_nonneg {d : ℕ} (M : ABKModel d) (m comparatorScale : ℤ) (s : { s : ℝ // 0 < s }) (omega : Cutoff.CutoffSample d) : 0 ≤ cutoffHomogenizationErrorAtComparatorScale M m comparatorScale s omega

The cutoff homogenization error with a separate comparator scale is pointwise nonnegative.

theorem Algsuperdiff.Section3.Observable.cutoffHomogenizationError_nonneg {d : ℕ} (M : ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) (omega : Cutoff.CutoffSample d) : 0 ≤ cutoffHomogenizationError M m s omega

The actual Section 3 cutoff homogenization error is pointwise nonnegative.

theorem Algsuperdiff.Section3.Observable.cutoffHomogenizationErrorAtComparatorScale_ae_eq_raw {d : ℕ} (M : ABKModel d) (m comparatorScale : ℤ) (s : { s : ℝ // 0 < s }) : cutoffHomogenizationErrorAtComparatorScale M m comparatorScale s =ᵐ[↑(Cutoff.cutoffSampleLaw M)] cutoffHomogenizationErrorRaw M m m (↑s) (Annealed.sigmaBar M comparatorScale)

The public observable with a separate comparator scale is almost everywhere the verified raw manuscript expression.

theorem Algsuperdiff.Section3.Observable.cutoffHomogenizationErrorAtComparatorScale_ae_eq_homogenizationErrorOnCube {d : ℕ} (M : ABKModel d) (m comparatorScale : ℤ) (s : { s : ℝ // 0 < s }) : cutoffHomogenizationErrorAtComparatorScale M m comparatorScale s =ᵐ[↑(Cutoff.cutoffSampleLaw M)] fun (omega : Cutoff.CutoffSample d) => HCPolySupport.Book.Ch02.HomogenizationErrorOnCube (HCPolySupport.originCube d m) (↑s) HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega) (isotropicComparatorMatrix (Annealed.sigmaBar M comparatorScale))

The public observable with a separate comparator scale is almost everywhere CoarseGraining's literal p = ∞, q = 2 homogenization error for a_m on \square_m, normalized by \bar\sigma_{\mathit{comparatorScale}}.

theorem Algsuperdiff.Section3.Observable.cutoffHomogenizationError_ae_eq_raw {d : ℕ} (M : ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) : cutoffHomogenizationError M m s =ᵐ[↑(Cutoff.cutoffSampleLaw M)] cutoffHomogenizationErrorRaw M m m (↑s) (Annealed.sigmaBar M m)

The actual Section 3 observable is almost everywhere its raw manuscript expression with coefficient, cube, and comparator scales all equal to m.

theorem Algsuperdiff.Section3.Observable.cutoffHomogenizationError_ae_eq_homogenizationErrorOnCube {d : ℕ} (M : ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) : cutoffHomogenizationError M m s =ᵐ[↑(Cutoff.cutoffSampleLaw M)] fun (omega : Cutoff.CutoffSample d) => HCPolySupport.Book.Ch02.HomogenizationErrorOnCube (HCPolySupport.originCube d m) (↑s) HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega) (isotropicComparatorMatrix (Annealed.sigmaBar M m))

The actual Section 3 observable is almost everywhere exactly \mathcal E_{s,\infty,2}(\square_m; a_m, \bar\sigma_m\operatorname{Id}) in CoarseGraining's literal source semantics.