High-contrast homogenization: Provider.PolynomialHomogenization.FractionalKernelBallScaling

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

Radius-sharp integrability of the interior fractional kernel

The shrinking-shell proof retains the radius in every shell, giving the homogeneous factor r^(e+d).

theorem HCPolySupport.HighContrast.exists_bound_lintegral_ball_rpow_scaled (d : ℕ) {e : ℝ} (hed : -↑d < e) (he0 : e < 0) : ∃ (C : ENNReal), C ≠ ⊤ ∧ ∀ (x : Vec d) {r : ℝ}, 0 < r → ∫⁻ (y : Vec d) in Metric.ball x r, ENNReal.ofReal (‖x - y‖ ^ e) ≤ C * ENNReal.ofReal (r ^ (e + ↑d))

A negative Riesz power above the dimensional threshold has its sharp homogeneous integral bound on every ball.