Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.RoundedAffineFields

High-contrast homogenization: Provider.Regularity.RoundedAffineFields #

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

Coefficient and field identities for the rounded affine map #

This is the algebraic core of the rounded affine transformation. It transforms the skew-centered physical coefficient, its symmetric reference, slopes, gradients, and the centered flux defect through the same lattice-compatible base rounded grid.

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

The source's rounded-coordinate coefficient: first remove the homogenized skew part and multiply by the exact scalar normalizer, then apply the rounded divergence-form pullback.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.roundedSymmetricReferenceCoefficient {d : ℕ} (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) :
    CoeffField d

    The rounded-coordinate constant symmetric reference.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem HCPolySupport.HighContrast.roundedSymmetricReferenceCoefficient_apply {d : ℕ} (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (y : Vec d) :
      roundedSymmetricReferenceCoefficient abar hS y = (baseRoundedGrid (symmPart abar))⁻¹ * specBound (symmPart abar)⁻¹ • symmPart abar * matTranspose (baseRoundedGrid (symmPart abar))⁻¹