Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.DeterministicNormalization

High-contrast homogenization: Provider.PolynomialHomogenization.DeterministicNormalization #

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

Deterministic identity normalization #

The inverse square root of a positive definite symmetric part normalizes that matrix to the positive scalar identity required by the deterministic coarse-graining comparison.

source
def HCPolySupport.HighContrast.identityConstantCoeffMatrix (d : ℕ) :
Book.Ch03.ConstantCoeffMatrix d

The identity comparison coefficient in the Chapter 3 carrier.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem HCPolySupport.HighContrast.identityConstantCoeffMatrix_matrix (d : ℕ) :
    (identityConstantCoeffMatrix d).matrix = 1

    The matrix carried by the identity comparison coefficient is the identity.

    source
    theorem HCPolySupport.HighContrast.identityConstantCoeffMatrix_isPositiveScalarMatrix (d : ℕ) :
    IsPositiveScalarMatrix (identityConstantCoeffMatrix d).matrix

    The identity comparison coefficient satisfies the upstream positivity contract.