High-contrast homogenization: Provider.PolynomialHomogenization.ConvexFractionalBallDomainMean

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

Core-ball and domain mean comparison

theorem HCPolySupport.HighContrast.ofReal_vecNormSq_coreMean_sub_domainMean_le {d : ℕ} (hd : 1 ≤ d) {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {c : Vec d} {rho Rad s : ℝ} (hrho : 0 < rho) (hRad : 0 < Rad) (hinner : euclideanBallAt c rho ⊆ U) (houter : U ⊆ euclideanBallAt c Rad) {G : Vec d → Vec d} (hGint : MeasureTheory.Integrable G (MeasureTheory.volume.restrict U)) (hs : 0 ≤ s) : ENNReal.ofReal (vecNormSq (volumeAverageVec (euclideanBallAt c rho) G - volumeAverageVec U G)) ≤ 2 * (convexHardyBallVolumeLower d rho)⁻¹ * ENNReal.ofReal ((2 * Rad) ^ (↑d + 2 * s)) * fracSeminormSq U s G

The core-ball mean differs from the domain mean by a structural multiple of the fractional energy.