High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.RowSupply.DescendantCoefficientRestriction
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Descendant restriction of a root coefficient identification #
The compatibility field of a triadic coefficient family transports an a.e. identification on a root cube to every descendant cube.
theorem
HCPolySupport.HighContrast.RowSupply.coeffOn_descendant_ae_eq_of_root_ae_eq
{d : ℕ}
(a : Book.Ch02.TriadicCoeffFamily d)
{Q R : TriadicCube d}
{k : ℤ}
(hk : k ≤ Q.scale)
(hR : R ∈ descendantsAtScale Q k)
{f : Vec d → Mat d}
(hroot : (a.coeffOn Q).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet Q)] f)
:
(a.coeffOn R).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet R)] f
A root-cube coefficient identification restricts to every descendant,
using the a.e. compatibility built into TriadicCoeffFamily.