High-contrast homogenization: Provider.PolynomialHomogenization.ConvexBoundaryDistanceLayer #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Boundary layers described by Euclidean distance #
The convex inner-boundary-layer estimate is converted into a weak L¹ tail
for the inverse Euclidean distance to the complement.
theorem
HCPolySupport.HighContrast.IsOpenBoundedConvexDomain.compl_nonempty
{d : ℕ}
(hd : 1 ≤ d)
{U : Set (Vec d)}
(hU : IsOpenBoundedConvexDomain U)
:
A bounded subset of a positive-dimensional vector space has nonempty complement.
theorem
HCPolySupport.HighContrast.euclideanBoundaryDistance_pos
{d : ℕ}
(hd : 1 ≤ d)
{U : Set (Vec d)}
(hU : IsOpenBoundedConvexDomain U)
{x : Vec d}
(hx : x ∈ U)
:
Euclidean boundary distance is positive in an open bounded domain.
theorem
HCPolySupport.HighContrast.euclideanBoundaryDistance_lt_iff_not_ball_subset
{d : ℕ}
(hd : 1 ≤ d)
{U : Set (Vec d)}
(hU : IsOpenBoundedConvexDomain U)
{x : Vec d}
{t : ℝ}
(ht : 0 ≤ t)
:
Boundary-distance sublevel sets are exactly the convex inner layers.
theorem
HCPolySupport.HighContrast.volume_euclideanBoundaryDistance_lt_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 ∧ euclideanBoundaryDistance U x < t} ≤ ENNReal.ofReal (↑d * t / rho) * MeasureTheory.volume U
The convex boundary layer controls Euclidean-distance sublevels.
theorem
HCPolySupport.HighContrast.measure_inverse_euclideanBoundaryDistance_gt_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.restrict U) {x : Vec d | t < (euclideanBoundaryDistance U x)⁻¹} ≤ ENNReal.ofReal (↑d * t⁻¹ / rho) * MeasureTheory.volume U
The inverse boundary distance has a weak L¹ tail on the domain.