Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.RoundedSymmetricReferenceEllipticity

High-contrast homogenization: Provider.Regularity.RoundedSymmetricReferenceEllipticity #

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Ellipticity of the rounded symmetric reference #

The rounded reference is not the identity. Its source-level matrix sandwich nevertheless gives the two coercivity inequalities required by IsEllipticMatrix: the lower bound is read directly, while the upper bound is reversed under matrix inversion.

source
theorem HCPolySupport.HighContrast.roundedSymmetricReferenceCoefficient_posDef {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (y : Vec d) :
Matrix.PosDef (roundedSymmetricReferenceCoefficient abar hS y)

The rounded symmetric reference is positive definite at every point.

source
theorem HCPolySupport.HighContrast.isEllipticMatrix_roundedSymmetricReferenceCoefficient {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (y : Vec d) :
IsEllipticMatrix (99 / 100) (101 / 100) (roundedSymmetricReferenceCoefficient abar hS y)

The near-identity rounded reference has the source's explicit ellipticity constants. In particular, this does not identify it with the exact-root identity coefficient.