High-contrast homogenization: #
Provider.PolynomialHomogenization.CorrectorDecayRestrictionComposition
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The restriction part of the physical corrector-decay transport #
The normalized negative-one restriction estimate applies simultaneously to the gradient and flux rows. Its affine-ellipsoid specialization below stops at the pulled-back ellipsoid: changing the negative-one norm itself through the affine map is a separate analytic statement.
theorem
HCPolySupport.HighContrast.negOneNorm_pair_le_sqrt_volumeRatio_of_subset
{d : ℕ}
[NeZero d]
{U V : Set (Vec d)}
(hUV : U ⊆ V)
(hU0 : MeasureTheory.volume U ≠ 0)
(hUtop : MeasureTheory.volume U ≠ ⊤)
(hV0 : MeasureTheory.volume V ≠ 0)
(hVtop : MeasureTheory.volume V ≠ ⊤)
(F G : Vec d → Vec d)
(hF : MemVectorL2 V F)
(hG : MemVectorL2 V G)
:
negOneNorm U F + negOneNorm U G ≤ ENNReal.ofReal √((MeasureTheory.volume V).toReal / (MeasureTheory.volume U).toReal) * (negOneNorm V F + negOneNorm V G)
Restricting two local square-integrable rows costs one common square-root volume ratio.