High-contrast homogenization: Provider.PolynomialHomogenization.ConvexBoundaryDistanceLipschitz

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

Lipschitz control of Euclidean boundary distance

theorem HCPolySupport.HighContrast.euclideanBoundaryDistance_le_add_euclideanDist {d : ℕ} (U : Set (Vec d)) (x y : Vec d) : euclideanBoundaryDistance U x ≤ euclideanBoundaryDistance U y + euclideanDist x y

Boundary distance changes by at most the Euclidean distance between its arguments.