High-contrast homogenization: Provider.PolynomialHomogenization.ConvexBoundaryDistance

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

Euclidean distance to the complement of a domain

The project vector carrier has the supremum norm. Fractional boundary weights use Euclidean distance, so the distance is taken in the project's Hilbert realization while retaining the ambient Vec carrier.

noncomputable def HCPolySupport.HighContrast.euclideanBoundaryDistance {d : ℕ} (U : Set (Vec d)) (x : Vec d) : ℝ

Euclidean distance from x to the complement of U. On an open domain this is the Euclidean distance to its boundary.

Equations

• HCPolySupport.HighContrast.euclideanBoundaryDistance U x = Metric.infDist (HCPolySupport.HilbertVec.ofVec x) (HCPolySupport.HilbertVec.ofVec '' Uᶜ)

theorem HCPolySupport.HighContrast.euclideanBoundaryDistance_nonneg {d : ℕ} (U : Set (Vec d)) (x : Vec d) : 0 ≤ euclideanBoundaryDistance U x

theorem HCPolySupport.HighContrast.continuous_euclideanBoundaryDistance {d : ℕ} (U : Set (Vec d)) : Continuous (euclideanBoundaryDistance U)

theorem HCPolySupport.HighContrast.measurable_euclideanBoundaryDistance {d : ℕ} (U : Set (Vec d)) : Measurable (euclideanBoundaryDistance U)

theorem HCPolySupport.HighContrast.euclideanBoundaryDistance_le_of_not_mem {d : ℕ} {U : Set (Vec d)} {x y : Vec d} (hy : y ∉ U) : euclideanBoundaryDistance U x ≤ euclideanDist x y

theorem HCPolySupport.HighContrast.euclideanBallAt_subset_of_le_boundaryDistance {d : ℕ} {U : Set (Vec d)} {x : Vec d} {r : ℝ} (hr : 0 ≤ r) (hreach : r ≤ euclideanBoundaryDistance U x) : euclideanBallAt x r ⊆ U

theorem HCPolySupport.HighContrast.not_subset_euclideanBallAt_of_boundaryDistance_lt {d : ℕ} {U : Set (Vec d)} (hcomp : Uᶜ.Nonempty) {x : Vec d} {r : ℝ} (hr : 0 ≤ r) (hreach : euclideanBoundaryDistance U x < r) : ¬euclideanBallAt x r ⊆ U