High-contrast homogenization: Provider.PolynomialHomogenization.ConvexBoundaryWeightLocalAllScales

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

Homogeneous local boundary moments at every radius

Small radii use convex localization. Large radii are absorbed by the global negative moment and the outer ball sandwich.

theorem HCPolySupport.HighContrast.exists_bound_lintegral_local_euclideanBoundaryWeight_all_scales {d : ℕ} (hd : 1 ≤ d) {rho Rad p : ℝ} (hrho : 0 < rho) (hRad : 0 < Rad) (hp0 : 0 < p) (hp1 : p < 1) : ∃ (C : ENNReal), C ≠ ⊤ ∧ ∀ (U : Set (Vec d)), IsOpenBoundedConvexDomain U → HasBallSandwich U rho Rad → ∀ (z : Vec d) {r : ℝ}, 0 < r → ∫⁻ (x : Vec d) in U ∩ euclideanBallAt z r, euclideanBoundaryWeight U p x ≤ C * ENNReal.ofReal (r ^ (↑d - p))

The homogeneous local negative boundary-distance moment holds for every positive radius, with one structural constant.