High-contrast homogenization: Provider.Regularity.AffinePullbackCoeffSpace #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Affine pullback of a qualitative coefficient sample #
An invertible divergence-form pullback is packaged on the existing
CoeffSpace carrier by its literal measurable representative. The
characterization theorem exposes that representative almost everywhere.
theorem
HCPolySupport.HighContrast.affinePullback_quasiMeasurePreserving
{d : ℕ}
(L : Mat d)
(hL : IsUnit (Matrix.det L))
:
theorem
HCPolySupport.HighContrast.affinePullback_aestronglyMeasurable
{d : ℕ}
(L : Mat d)
(hL : IsUnit (Matrix.det L))
{b : CoeffField d}
(hb : MeasureTheory.AEStronglyMeasurable b MeasureTheory.volume)
:
theorem
HCPolySupport.HighContrast.affinePullback_isEllipticMatrix
{d : ℕ}
(L : Mat d)
(hL : IsUnit (Matrix.det L))
{b : CoeffField d}
{lam Lam : ℝ}
{y : Vec d}
(hb : IsEllipticMatrix lam Lam (b (matVecMul L y)))
:
IsEllipticMatrix (lam / max 1 (Book.Ch02.matrixFrobeniusNormSq (matTranspose L)))
(max Lam (Book.Ch02.matrixFrobeniusNormSq L⁻¹ * Lam)) (affineCoefficient L hL b y)
noncomputable def
HCPolySupport.HighContrast.affinePullbackCoeffSpace
{d : ℕ}
(L : Mat d)
(hL : IsUnit (Matrix.det L))
(a : CoeffSpace d)
:
The literal affine pullback of one qualitative coefficient sample.
Equations
Instances For
theorem
HCPolySupport.HighContrast.affinePullbackCoeffSpace_ae
{d : ℕ}
(L : Mat d)
(hL : IsUnit (Matrix.det L))
(a : CoeffSpace d)
:
↑↑(affinePullbackCoeffSpace L hL a) =ᵐ[MeasureTheory.volume] affineCoefficient L hL ↑↑a
The packaged sample has exactly the divergence-form pullback as its a.e. representative.
theorem
HCPolySupport.HighContrast.affineCoefficient_congr_ae
{d : ℕ}
(L : Mat d)
(hL : IsUnit (Matrix.det L))
{a b : CoeffField d}
(hab : a =ᵐ[MeasureTheory.volume] b)
:
affineCoefficient L hL a =ᵐ[MeasureTheory.volume] affineCoefficient L hL b
Affine pullback respects almost-everywhere equality of coefficient representatives.