High-contrast homogenization: Provider.Quenched.Prop42CanonicalMetric #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Canonical-grid eccentricity for the small-contrast argument #
The adapted grid in the perturbative argument is matched to the canonical metric of the reference block. Its eccentricity is controlled by the reference aspect ratio, so the geometry introduces no dependence on the private ellipticity constants of a coefficient field.
theorem
HCPolySupport.HighContrast.Quenched.witnessEccentricity_canonicalMetric_le_aspectRatio
{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)
:
The canonical metric of a coarse-ellipticity reference block has eccentricity at most the reference aspect ratio.