High-contrast homogenization: Provider.PolynomialHomogenization.ConvexBoundaryWeightNearComparison

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

Boundary-weight comparison near an interior point

theorem HCPolySupport.HighContrast.half_euclideanBoundaryDistance_le_of_mem_ball {d : ℕ} (U : Set (Vec d)) {x y : Vec d} (hx : 0 < euclideanBoundaryDistance U x) (hy : y ∈ euclideanBallAt x (euclideanBoundaryDistance U x / 2)) : euclideanBoundaryDistance U x / 2 ≤ euclideanBoundaryDistance U y

Inside half the boundary distance from x, boundary distance remains at least half its value at x.

theorem HCPolySupport.HighContrast.euclideanBoundaryWeight_le_of_mem_half_ball {d : ℕ} (U : Set (Vec d)) {p : ℝ} (hp : 0 ≤ p) {x y : Vec d} (hx : 0 < euclideanBoundaryDistance U x) (hy : y ∈ euclideanBallAt x (euclideanBoundaryDistance U x / 2)) : euclideanBoundaryWeight U p y ≤ ENNReal.ofReal ((euclideanBoundaryDistance U x / 2) ^ (-p))

A negative boundary-distance weight is uniformly controlled on the ball of half the center boundary distance.