CutoffHomogenizationErrorRaw

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

Literal cutoff homogenization-error observable

This file records the raw, pointwise manuscript expression \mathcal E_{s,\infty,2}(\square_m; a_L, \sigma \operatorname{Id}) on the canonical cutoff-sample carrier. The coefficient scale L and the observed cube scale m are deliberately separate arguments.

It is deliberately not itself the measurable representative. The companion module CutoffHomogenizationErrorRepresentative constructs the genuine nonnegative measurable representative and proves its explicit almost-everywhere identity with this literal expression. Keeping the raw expression separate prevents a measurable modification from being mistaken for the manuscript observable.

References

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

noncomputable def Algsuperdiff.Section3.Observable.cutoffHomogenizationErrorRaw {d : ℕ} (M : ABKModel d) (coefficientScale domainScale : ℤ) (s : ℝ) (sigma : PositiveScalar) (omega : Cutoff.CutoffSample d) : ℝ

The literal cutoff expression \mathcal E_{s,\infty,2}(\square_m; a_L, \sigma \operatorname{Id}).

coefficientScale specifies the actual lower-infinite cutoff coefficient a_L, while domainScale specifies the cube \square_m; neither scale is silently substituted for the other.

Equations

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

theorem Algsuperdiff.Section3.Observable.cutoffHomogenizationErrorRaw_characterization {d : ℕ} (M : ABKModel d) (coefficientScale domainScale : ℤ) (s : ℝ) (sigma : PositiveScalar) (omega : Cutoff.CutoffSample d) : cutoffHomogenizationErrorRaw M coefficientScale domainScale s sigma omega = HCPolySupport.Book.Ch02.HomogenizationErrorOnCube (HCPolySupport.originCube d domainScale) s HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Cutoff.coefficientCutoffTriadicCoeffFamily M coefficientScale omega) (isotropicComparatorMatrix sigma)

The raw cutoff expression is exactly the manuscript's homogenization error on the genuine compatible cutoff family.

theorem Algsuperdiff.Section3.Observable.cutoffHomogenizationErrorRaw_nonneg {d : ℕ} (M : ABKModel d) (coefficientScale domainScale : ℤ) {s : ℝ} (hs : 0 < s) (sigma : PositiveScalar) (omega : Cutoff.CutoffSample d) : 0 ≤ cutoffHomogenizationErrorRaw M coefficientScale domainScale s sigma omega

The literal cutoff homogenization error is nonnegative.