High-contrast homogenization: Provider.PolynomialHomogenization.ConvexBoundaryWeightLocalScaling #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Homogeneous local boundary-weight moments #
theorem
HCPolySupport.HighContrast.exists_bound_lintegral_local_euclideanBoundaryWeight_scaled
{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 →
r ≤ Rad →
(U ∩ euclideanBallAt z r).Nonempty →
∫⁻ (x : Vec d) in U ∩ euclideanBallAt z r, euclideanBoundaryWeight U p x ≤ C * ENNReal.ofReal (r ^ (↑d - p))
The local negative boundary-distance moment has homogeneous order
d-p, uniformly over the center and radius.