High-contrast homogenization: Analytic.SingularKernel

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

The Gagliardo kernel is uniformly integrable on balls

The fractional seminorm of e.physical.fractional.norm is a double integral whose inner integrand is

|ψ(x) - ψ(y)|² / |x - y|^{d + 2s}.

For a Lipschitz field the numerator is O(‖x - y‖²), so the integrand is dominated by the Riesz-type kernel ‖x - y‖^{2 - (d + 2s)} with exponent e = 2 - (d + 2s) > -d exactly when s < 1. This module supplies the two ingredients of that reduction:

• a bound on ∫ ‖x - y‖^e dy over the ball of radius D centred at x that is independent of the centre and finite for every e > -d;
• the pointwise domination of the Gagliardo integrand by that kernel.

The integral bound is proved by a dyadic decomposition into the shells 2^{-k-1} ≤ ‖x - y‖ < 2^{-k}, on each of which the integrand is bounded by its value on the inner sphere and the shell is contained in a ball of known volume. The resulting series is geometric with ratio 2^{-(e + d)} < 1. No polar-coordinate machinery is used, and every bound is centre-independent because the ambient balls all have the same volume.

The singular kernel is uniformly integrable on balls

theorem HCPolySupport.HighContrast.exists_bound_lintegral_ball_rpow (d : ℕ) {D e : ℝ} (hD : 0 < D) (he : -↑d < e) : ∃ (B : ENNReal), B ≠ ⊤ ∧ ∀ (x : Vec d), ∫⁻ (y : Vec d) in Metric.ball x D, ENNReal.ofReal (‖x - y‖ ^ e) ≤ B

The pointwise bound on the Gagliardo kernel

theorem HCPolySupport.HighContrast.gagliardo_kernel_le {d : ℕ} {ψ : Vec d → Vec d} {L : ℝ} (hlip : ∀ (x y : Vec d), ‖ψ x - ψ y‖ ≤ L * ‖x - y‖) {p : ℝ} (hp : 0 ≤ p) (x y : Vec d) : vecNormSq (ψ x - ψ y) / √(vecNormSq (x - y)) ^ p ≤ ↑d * L ^ 2 * ‖x - y‖ ^ (2 - p)