High-contrast homogenization:

Provider.PolynomialHomogenization.ConvexBoundaryWeightedCenteredEndpoint

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Boundary-weighted centered fractional endpoint

theorem HCPolySupport.HighContrast.euclideanBoundaryWeightedCenteredEnergy_le_around_add_meanShift {d : ℕ} {U : Set (Vec d)} {G : Vec d → Vec d} (hG : MeasureTheory.Integrable G (MeasureTheory.volume.restrict U)) (p : ℝ) (m : Vec d) : euclideanBoundaryWeightedCenteredEnergy U p G ≤ 2 * euclideanBoundaryWeightedEnergyAround U p G m + 2 * ENNReal.ofReal (vecNormSq (m - volumeAverageVec U G)) * euclideanBoundaryWeightMoment U p

Centering at the domain mean costs the weighted energy around any reference vector plus its squared displacement from the domain mean.