High-contrast homogenization: Provider.Regularity.RoundedCenteredCoeffSpace #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Rounded centered qualitative coefficient sample #
The skew-centered and exactly normalized coefficient is pulled back through
the base rounded grid and packaged on the existing CoeffSpace carrier. The
characterization theorem identifies its representative with the rounded
coefficient field used by the affine response transfer.
theorem
HCPolySupport.HighContrast.normalizedCenteredCoeff_ae
{d : ℕ}
[NeZero d]
(a : CoeffSpace d)
(abar : Mat d)
(hS : Matrix.PosDef (symmPart abar))
:
↑↑(normalizedCenteredCoeff a abar hS) =ᵐ[MeasureTheory.volume] fun (x : Vec d) =>
specBound (symmPart abar)⁻¹ • (↑↑a x - skewPart abar)
The normalized centered coefficient has its literal pointwise representative almost everywhere.
noncomputable def
HCPolySupport.HighContrast.roundedCenteredCoeffSpace
{d : ℕ}
[NeZero d]
(abar : Mat d)
(hS : Matrix.PosDef (symmPart abar))
(a : CoeffSpace d)
:
The qualitative coefficient sample in the source's rounded centered coordinates.
Equations
- One or more equations did not get rendered due to their size.