High-contrast homogenization: Annealed.Positivity #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Positivity of the annealed block under the coarse ellipticity assumption #
The annealed block at a centered cube is the expectation of a family of positive
definite coarse responses, and is therefore itself positive definite: the
well-formedness that e.Theta.m presupposes for Θ_m.
theorem
HCPolySupport.HighContrast.blockPosDef_annealedBlock_of_coarseEllipticityDagger
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{g : ℝ}
{E : BlockMat d}
{Ψ : ℝ → ℝ}
{K : ℝ}
{S : CoeffSpace d → ℝ}
(hdag : CoarseEllipticityDagger P g E Ψ K S)
(m : ℤ)
:
Book.Ch02.BlockPosDef (annealedBlock P (centeredCube d m))
The positivity of the annealed block under e.coarse.ellipticity:
the annealed block at every scale is the honest expectation of a positive
definite family, and is itself positive definite.