High-contrast homogenization: Provider.PolynomialHomogenization.ConvexHardyLocalLayer

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

Local boundary layers of convex domains

A ball sandwich of a convex domain remains quantitatively useful after localization. The localization used here intersects the domain with an ambient metric ball. A point in the corresponding Euclidean ball is shifted a short distance toward the center of the sandwich; convexity then supplies an interior Euclidean ball at the shifted point.

The resulting local sandwich turns the global convex boundary-layer estimate into an explicit estimate on every Euclidean localization.

theorem HCPolySupport.HighContrast.euclideanBallAt_dilate_subset_of_convex {d : ℕ} {U : Set (Vec d)} (hconv : Convex ℝ U) {c : Vec d} {rho lam : ℝ} (hrho : 0 < rho) (hball : euclideanBallAt c rho ⊆ U) (hlam : lam ∈ Set.Ico 0 1) {x : Vec d} (hx : x ∈ U) : euclideanBallAt (c + lam • (x - c)) ((1 - lam) * rho) ⊆ U

Dilating a point of a convex set toward the center of an interior ball produces another interior ball, with the complementary dilation factor as its radius factor.

theorem HCPolySupport.HighContrast.IsOpenBoundedConvexDomain.inter_metricBall {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (z : Vec d) (r : ℝ) : IsOpenBoundedConvexDomain (U ∩ Metric.ball z r)

Intersecting a bounded open convex domain with an ambient ball preserves the domain class.

theorem HCPolySupport.HighContrast.hasBallSandwich_inter_metricBall {d : ℕ} (hd : 1 ≤ d) {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {rho Rad r : ℝ} (hsand : HasBallSandwich U rho Rad) (hr : 0 < r) (hrRad : r ≤ Rad) {z : Vec d} (hne : (U ∩ euclideanBallAt z r).Nonempty) : HasBallSandwich (U ∩ Metric.ball z (2 * r)) (r * rho / (4 * (rho + Rad))) (4 * r * √↑d)

A nonempty Euclidean localization of a convex ball-sandwiched domain gives an explicit ball sandwich for the domain intersected with the doubled ambient ball.