High-contrast homogenization: Provider.PolynomialHomogenization.ConvexBoundaryWeightLocalMoment #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Local negative moments of convex boundary distance #
The global negative-moment estimate is applied to a doubled ball localization. Monotonicity of boundary distance then controls the original domain weight on the smaller localization.
theorem
HCPolySupport.HighContrast.euclideanBoundaryWeight_mono_of_subset
{d : ℕ}
(hd : 1 ≤ d)
{V U : Set (Vec d)}
(hV : IsOpenBoundedConvexDomain V)
(hU : IsOpenBoundedConvexDomain U)
(hVU : V ⊆ U)
{p : ℝ}
(hp : 0 ≤ p)
{x : Vec d}
(hx : x ∈ V)
:
On a smaller open bounded convex domain, the negative boundary-distance weight dominates that of the larger domain.
theorem
HCPolySupport.HighContrast.lintegral_local_euclideanBoundaryWeight_le
{d : ℕ}
(hd : 1 ≤ d)
{U : Set (Vec d)}
(hU : IsOpenBoundedConvexDomain U)
{rho Rad r p : ℝ}
(hsand : HasBallSandwich U rho Rad)
(hr : 0 < r)
(hrRad : r ≤ Rad)
(hp0 : 0 < p)
(hp1 : p < 1)
{z : Vec d}
(hne : (U ∩ euclideanBallAt z r).Nonempty)
:
∫⁻ (x : Vec d) in U ∩ euclideanBallAt z r, euclideanBoundaryWeight U p x ≤ MeasureTheory.volume (Metric.ball z (2 * r)) * ENNReal.ofReal ((↑d / (r * rho / (4 * (rho + Rad)))) ^ p / (1 - p))
A ball localization has the scale-correct negative boundary-distance moment, expressed using the volume of its doubled metric ball.