High-contrast homogenization: Provider.PolynomialHomogenization.ConvexBoundaryWeightAlgebra

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

Algebra of negative boundary-distance weights

theorem HCPolySupport.HighContrast.euclideanBoundaryWeight_mul {d : ℕ} {U : Set (Vec d)} {x : Vec d} (hx : 0 < euclideanBoundaryDistance U x) (p q : ℝ) : euclideanBoundaryWeight U p x * euclideanBoundaryWeight U q x = euclideanBoundaryWeight U (p + q) x

Negative boundary-distance weights multiply by adding their orders at points of positive boundary distance.

theorem HCPolySupport.HighContrast.euclideanBoundaryWeight_mul_ofReal_rpow_sub {d : ℕ} {U : Set (Vec d)} {x : Vec d} (hx : 0 < euclideanBoundaryDistance U x) (s a : ℝ) : euclideanBoundaryWeight U s x * ENNReal.ofReal (euclideanBoundaryDistance U x ^ (s - a)) = euclideanBoundaryWeight U a x

Multiplying an order-s boundary weight by delta^(s-a) leaves the order-a boundary weight.