High-contrast homogenization: Provider.PolynomialHomogenization.ConvexBoundaryLayer

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

Boundary layers of convex domains

An interior Euclidean ball controls the volume of every inner boundary layer of a convex domain. The proof places a homothetic copy of the domain inside the complementary inner core and compares its volume with the original one.

theorem HCPolySupport.HighContrast.volume_innerBoundaryLayer_le {d : ℕ} (hd : 1 ≤ d) {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {rho Rad t : ℝ} (hsand : HasBallSandwich U rho Rad) (ht : 0 ≤ t) : MeasureTheory.volume {x : Vec d | x ∈ U ∧ ¬euclideanBallAt x t ⊆ U} ≤ ENNReal.ofReal (↑d * t / rho) * MeasureTheory.volume U

The volume within Euclidean distance t of the inside boundary of a bounded open convex domain is at most d t / rho times the domain volume, when the domain contains a concentric Euclidean ball of radius rho.