HomogenizationErrorLocality

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

Root locality of CoarseGraining's homogenization error

The raw origin-cube homogenization error depends only on the coefficient on that cube, not on a chosen compatible global family.

theorem Algsuperdiff.Section24.UnitCubeMultiscale.homogenizationErrorOnCube_eq_of_root_aeeq {d : ℕ} (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (F G : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a) (hG : (G.coeffOn (HCPolySupport.originCube d 0)).AEEq a) (s : ℝ) (p q : HCPolySupport.Book.Ch02.MultiscaleExponent) (a0 : HCPolySupport.Mat d) : HCPolySupport.Book.Ch02.HomogenizationErrorOnCube (HCPolySupport.originCube d 0) s p q F a0 = HCPolySupport.Book.Ch02.HomogenizationErrorOnCube (HCPolySupport.originCube d 0) s p q G a0

CoarseGraining's raw homogenization error at the origin depends only on the origin coefficient.