Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.RoundedReferenceConstantMatrix

High-contrast homogenization: Provider.Regularity.RoundedReferenceConstantMatrix #

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

Constant-matrix package for the rounded reference #

The rounded coordinate change produces a constant symmetric reference that is near, but not equal, to the identity. This module packages that reference in the Chapter 3 constant-coefficient carrier with the source's explicit ellipticity constants.

source
noncomputable def HCPolySupport.HighContrast.roundedReferenceMatrix {d : ℕ} (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) :
Mat d

The matrix value of the constant rounded symmetric reference.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.roundedSymmetricReferenceCoefficient_apply_eq_roundedReferenceMatrix {d : ℕ} (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (y : Vec d) :
    roundedSymmetricReferenceCoefficient abar hS y = roundedReferenceMatrix abar hS

    The rounded symmetric reference field is constant with the selected matrix value.

    source
    theorem HCPolySupport.HighContrast.roundedReferenceMatrix_posDef {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) :
    Matrix.PosDef (roundedReferenceMatrix abar hS)

    The selected rounded reference matrix is positive definite.

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

    The selected rounded reference matrix has the exact near-identity ellipticity constants used by the regularity black box.

    source
    noncomputable def HCPolySupport.HighContrast.roundedReferenceConstantCoeffMatrix {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) :
    Book.Ch03.ConstantCoeffMatrix d

    The genuinely rounded comparison matrix in the Chapter 3 constant-coefficient carrier.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem HCPolySupport.HighContrast.roundedReferenceConstantCoeffMatrix_matrix {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) :
      (roundedReferenceConstantCoeffMatrix abar hS).matrix = roundedReferenceMatrix abar hS
      source
      theorem HCPolySupport.HighContrast.constantCoeffField_roundedReferenceConstantCoeffMatrix {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) :
      constantCoeffField (roundedReferenceConstantCoeffMatrix abar hS).matrix = roundedSymmetricReferenceCoefficient abar hS

      The Chapter 3 constant field is exactly the rounded symmetric reference, not the scalar identity field.