Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section24.UnitCubeMultiscale.BigLambda.Characterization

Characterization #

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

Characterization of origin-cube upper multiscale ellipticity #

source
theorem Algsuperdiff.Section24.UnitCubeMultiscale.BigLambda.characterization {d : ℕ} (s : ℝ) (q : HCPolySupport.Book.Ch02.MultiscaleExponent) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) :
(F.coeffOn (HCPolySupport.originCube d 0)).AEEq a → Frozen.Section24.unitCubeBigLambda s q a = HCPolySupport.Book.Ch02.LambdaSq (HCPolySupport.originCube d 0) s q F

The unique-choice characterization used by the corresponding frozen theorem.