HomogenizationError

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

Section 3 homogenization-error observable

This file defines the precise Section 3 specialization

mathcal E_{s,infinity,2}(square_m; a, sigma Id)

for an actual coefficient restriction a on square_m and a strictly positive scalar comparator sigma. The coefficient is pulled back by x ↦ 3^m x to the unit cube and then fed to the already frozen, fully characterized unit-cube homogenization error. Thus the definition uses the paper's spatial exponent p = infinity, aggregation exponent q = 2, and the literal sigma Id gauge. There is no free error family or fallback.

References

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

noncomputable def Algsuperdiff.Section3.Observable.homogenizationErrorAtScale {d : ℕ} (m : ℤ) (s : ℝ) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d m))) (sigma : PositiveScalar) : ℝ

The exact Section 3 error mathcal E_{s,infinity,2}(square_m; a, sigma Id).

Equations

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

theorem Algsuperdiff.Section3.Observable.homogenizationErrorAtScale_characterization {d : ℕ} (m : ℤ) (s : ℝ) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d m))) (sigma : PositiveScalar) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d m)).AEEq a) : homogenizationErrorAtScale m s a sigma = HCPolySupport.Book.Ch02.HomogenizationErrorOnCube (HCPolySupport.originCube d m) s HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) F (isotropicComparatorMatrix sigma)

Characterization by the manuscript's literal mathcal E_{s,infinity,2} on square_m. The equality also certifies that the scalar gauge is sigma Id, with no bare-diffusivity substitution.

theorem Algsuperdiff.Section3.Observable.homogenizationErrorAtScale_nonneg {d : ℕ} (m : ℤ) {s : ℝ} (hs : 0 < s) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d m))) (sigma : PositiveScalar) : 0 ≤ homogenizationErrorAtScale m s a sigma

The Section 3 homogenization error is nonnegative. This follows directly from the finite-q Real.rpow branch of CoarseGraining's literal definition.