High-contrast homogenization: Provider.PolynomialHomogenization.ConvexFractionalChainPotential #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Riesz-potential aggregation of the infinite convex chain #
The explicit structural factor in the physical chain-membership kernel.
Equations
- HCPolySupport.HighContrast.convexFractionalChainRieszConstant rho Rad a = ENNReal.ofReal ((2 * Rad) ^ a) + ENNReal.ofReal ((Rad + rho) ^ a) * ENNReal.ofReal (2 ^ a / (2 ^ a - 1))
Instances For
theorem
HCPolySupport.HighContrast.tsum_convexFractionalChainBall_scaleWeight_le_rieszKernel
{d : ℕ}
{U : Set (Vec d)}
{c x y : Vec d}
{rho Rad s : ℝ}
(hrho : 0 < rho)
(hRad : 0 < Rad)
(houter : U ⊆ euclideanBallAt c Rad)
(hx : x ∈ U)
(hy : y ∈ U)
(hxy : x ≠ y)
(hsd : s < ↑d)
:
∑' (n : ℕ), (convexFractionalChainBall c x rho n).indicator
(fun (x : Vec d) => ENNReal.ofReal (convexFractionalChainScale n ^ (s - ↑d))) y ≤ convexFractionalChainRieszConstant rho Rad (↑d - s) * ENNReal.ofReal (euclideanDist x y ^ (s - ↑d))
The pointwise chain-membership series is bounded by the physical
order-d-s Riesz kernel away from the diagonal.
theorem
HCPolySupport.HighContrast.tsum_scaleWeight_mul_chainAmplitude_le_rieszPotential
{d : ℕ}
(hd : 1 ≤ d)
{U : Set (Vec d)}
(hU : IsOpenBoundedConvexDomain U)
{c x : Vec d}
{rho Rad s : ℝ}
(hrho : 0 < rho)
(hRad : 0 < Rad)
(hinner : euclideanBallAt c rho ⊆ U)
(houter : U ⊆ euclideanBallAt c Rad)
(hx : x ∈ U)
{G : Vec d → Vec d}
(hG : Measurable G)
(hsd : s < ↑d)
:
∑' (n : ℕ), ENNReal.ofReal (convexFractionalChainScale n ^ (s - ↑d)) * ∫⁻ (y : Vec d) in convexFractionalChainBall c x rho n, fractionalGagliardoAmplitude U s G y ≤ convexFractionalChainRieszConstant rho Rad (↑d - s) * ∫⁻ (y : Vec d) in U, ENNReal.ofReal (euclideanDist x y ^ (s - ↑d)) * fractionalGagliardoAmplitude U s G y
Summing the weighted amplitude masses of all chain balls gives a Riesz potential of the global amplitude.