Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.FractionalBoundaryWeightedRieszKernel

High-contrast homogenization: #

Provider.PolynomialHomogenization.FractionalBoundaryWeightedRieszKernel

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

Fractional Riesz kernel against a convex boundary weight #

theorem HCPolySupport.HighContrast.exists_bound_lintegral_fractionalBoundaryRieszKernel {d : ℕ} (hd : 1 ≤ d) {rho Rad s p : ℝ} (hrho : 0 < rho) (hRad : 0 < Rad) (hs : 0 < s) (hsp : s < p) (hp1 : p < 1) :
∃ (C : ENNReal), C ≠ ⊤ ∧ ∀ (U : Set (Vec d)), IsOpenBoundedConvexDomain U → HasBallSandwich U rho Rad → ∀ x ∈ U, ∫⁻ (y : Vec d) in U, ENNReal.ofReal (euclideanDist x y ^ (s - ↑d)) * euclideanBoundaryWeight U p y ≤ C * ENNReal.ofReal (euclideanBoundaryDistance U x ^ (s - p))

The complete Riesz potential of delta^(-p) has homogeneous order delta^(s-p) for 0<s<p<1.