EllipticityLocality

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

Root locality of CoarseGraining multiscale ellipticity

The lower and upper multiscale ellipticity values at the origin cube depend only on the coefficient there, not on a chosen compatible global family.

theorem Algsuperdiff.Section24.UnitCubeMultiscale.bigLambdaSq_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 : ℝ) (q : HCPolySupport.Book.Ch02.MultiscaleExponent) : HCPolySupport.Book.Ch02.LambdaSq (HCPolySupport.originCube d 0) s q F = HCPolySupport.Book.Ch02.LambdaSq (HCPolySupport.originCube d 0) s q G

CoarseGraining's raw upper multiscale ellipticity at the origin depends only on the origin coefficient.

theorem Algsuperdiff.Section24.UnitCubeMultiscale.lambdaSq_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 : ℝ) (q : HCPolySupport.Book.Ch02.MultiscaleExponent) : HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d 0) s q F = HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d 0) s q G

CoarseGraining's raw lower multiscale ellipticity at the origin depends only on the origin coefficient.