High-contrast homogenization: Provider.Regularity.RoundedEllipsoidWeightedNormBridge #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Normalized weighted-energy transfer across rounded real-radius domains #
This module supplies the measure-normalization part of the Lane-C terminal
consumer. Every comparison is between the exact rounded pullback ellipsoid
and the exact origin cubes selected by RoundedEllipsoidTriadicGeometry.
The constants are deliberately coarse and depend only on the dimension.
theorem
HCPolySupport.HighContrast.weightedGradNorm_mono_set_le_volumeRatio
{d : ℕ}
{U V : Set (Vec d)}
(hUV : U ⊆ V)
(hUzero : MeasureTheory.volume U ≠ 0)
(hUtop : MeasureTheory.volume U ≠ ⊤)
(hVzero : MeasureTheory.volume V ≠ 0)
(hVtop : MeasureTheory.volume V ≠ ⊤)
(b : CoeffField d)
(F : Vec d → Vec d)
:
weightedGradNorm b U F ≤ (MeasureTheory.volume V / MeasureTheory.volume U) ^ (1 / 2) * weightedGradNorm b V F
Restricting a normalized weighted gradient norm to a smaller positive finite-volume set costs the square root of the volume ratio.