High-contrast homogenization: Provider.Quenched.TriadicRebasedDagger #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Coarse ellipticity under triadic rebasing #
The coarse ellipticity carrier is transported directly through the measurable coefficient-space dilation. Both spatial generations shift by the same integer, so the discount exponent is unchanged.
theorem
HCPolySupport.HighContrast.standardCellCenter_add_mem_centeredCube_add
{d : ℕ}
(n : ℕ)
{m k : ℤ}
{w : Fin d → ℤ}
(hcenter : standardCellCenter k w ∈ centeredCube d m)
:
Dilating both generations preserves membership of a standard-cell center in the corresponding centered cube.
theorem
HCPoly.Frozen.CoarseEllipticityDagger.triadicRebased
{d : ℕ}
{P : MeasureTheory.Measure (HCPolySupport.HighContrast.CoeffSpace d)}
{g : ℝ}
{E : HCPolySupport.BlockMat d}
{Ψ : ℝ → ℝ}
{K : ℝ}
{S : HCPolySupport.HighContrast.CoeffSpace d → ℝ}
(hdagger : CoarseEllipticityDagger P g E Ψ K S)
(n : ℕ)
:
Coarse ellipticity on the frozen coefficient-law carrier is preserved by triadic rebasing, with the source and gauge expressed in the rebased units.