HolderGagliardoRadial

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The radial kernel integral ∫_{B(x,R)} |x-y|^{-β} dy

Nothing here imports that file, nothing here claims the anchor, and nothing here is a frozen statement.

The target

This file proves the sharp-in-R bound, with the explicit constant, in the ambient supremum metric of Vec d:

  ∫_{B(x,R)} |x-y|^{-β} dy  ≤  ( 2^d 3^β / (1 - 3^{β-d}) ) · R^{d-β}
        for  0 < β < d .

Everything is ℝ≥0∞-valued, so no integrability side condition is needed.

The mechanism

The ball is covered by the point x (where the integrand is the junk value 0^{-β} = 0) together with the triadic annuli A_i = { R·3^{-i-1} ≤ |x-y| < R·3^{-i} }. On A_i the integrand is at most (R·3^{-i-1})^{-β} and |A_i| ≤ (2·R·3^{-i})^d, so the i-th contribution is T_i = (^{-i-1})^{-β} (2^{-i})^d, a geometric sequence of ratio 3^{β}/3^{d} < 1.

References

• ABK26, t.regularity Step 4, (the two seminorm comparisons stated without proof).
• ABK26, (the fractional Sobolev seminorm) (the Hölder seminorm and the p = ∞ convention).

1. The triadic annuli around a point

noncomputable def Algsuperdiff.Section4.Provider.Regularity.annulusRadius (R : ℝ) (i : ℕ) : ℝ

The radius R · 3^{-i} of the i-th triadic shell.

Equations

• Algsuperdiff.Section4.Provider.Regularity.annulusRadius R i = R * 3 ^ (-↑i)

theorem Algsuperdiff.Section4.Provider.Regularity.annulusRadius_zero (R : ℝ) : annulusRadius R 0 = R

theorem Algsuperdiff.Section4.Provider.Regularity.annulusRadius_pos {R : ℝ} (hR : 0 < R) (i : ℕ) : 0 < annulusRadius R i

theorem Algsuperdiff.Section4.Provider.Regularity.annulusRadius_succ (R : ℝ) (i : ℕ) : annulusRadius R (i + 1) = annulusRadius R i / 3

theorem Algsuperdiff.Section4.Provider.Regularity.annulusRadius_eq_pow (R : ℝ) (i : ℕ) : annulusRadius R i = R * (1 / 3) ^ i

def Algsuperdiff.Section4.Provider.Regularity.triadicAnnulus {d : ℕ} (x : HCPolySupport.Vec d) (R : ℝ) (i : ℕ) : Set (HCPolySupport.Vec d)

The i-th triadic annulus { R·3^{-i-1} ≤ |x-y| < R·3^{-i} } around x.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.Regularity.measurableSet_triadicAnnulus {d : ℕ} (x : HCPolySupport.Vec d) (R : ℝ) (i : ℕ) : MeasurableSet (triadicAnnulus x R i)

theorem Algsuperdiff.Section4.Provider.Regularity.triadicAnnulus_subset_ball {d : ℕ} (x : HCPolySupport.Vec d) (R : ℝ) (i : ℕ) : triadicAnnulus x R i ⊆ Metric.ball x (annulusRadius R i)

theorem Algsuperdiff.Section4.Provider.Regularity.ball_subset_singleton_union_triadicAnnulus {d : ℕ} (x : HCPolySupport.Vec d) {R : ℝ} (hR : 0 < R) : Metric.ball x R ⊆ {x} ∪ ⋃ (i : ℕ), triadicAnnulus x R i

The annuli cover the punctured ball. The centre is separated out because the integrand takes the junk value 0^{-β} = 0 there.

2. The geometric sequence of shell contributions

noncomputable def Algsuperdiff.Section4.Provider.Regularity.annulusTerm (d : ℕ) (R beta : ℝ) (i : ℕ) : ℝ

T_i = (R·3^{-i-1})^{-β} · (2·R·3^{-i})^d, the i-th shell contribution.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section4.Provider.Regularity.annulusRatio (d : ℕ) (beta : ℝ) : ℝ

The common ratio 3^β / 3^d of the shell contributions.

Equations

• Algsuperdiff.Section4.Provider.Regularity.annulusRatio d beta = 3 ^ beta / 3 ^ d

theorem Algsuperdiff.Section4.Provider.Regularity.annulusRatio_pos (d : ℕ) (beta : ℝ) : 0 < annulusRatio d beta

theorem Algsuperdiff.Section4.Provider.Regularity.annulusRatio_lt_one {d : ℕ} {beta : ℝ} (hbd : beta < ↑d) : annulusRatio d beta < 1

theorem Algsuperdiff.Section4.Provider.Regularity.annulusTerm_pos {d : ℕ} {R : ℝ} (hR : 0 < R) (beta : ℝ) (i : ℕ) : 0 < annulusTerm d R beta i

theorem Algsuperdiff.Section4.Provider.Regularity.annulusTerm_succ {d : ℕ} {R : ℝ} (hR : 0 < R) (beta : ℝ) (i : ℕ) : annulusTerm d R beta (i + 1) = annulusRatio d beta * annulusTerm d R beta i

theorem Algsuperdiff.Section4.Provider.Regularity.annulusTerm_eq_geometric {d : ℕ} {R : ℝ} (hR : 0 < R) (beta : ℝ) (i : ℕ) : annulusTerm d R beta i = annulusTerm d R beta 0 * annulusRatio d beta ^ i

3. The shell estimate

theorem Algsuperdiff.Section4.Provider.Regularity.volume_triadicAnnulus_le {d : ℕ} {x : HCPolySupport.Vec d} {R : ℝ} (hR : 0 < R) (i : ℕ) : MeasureTheory.volume (triadicAnnulus x R i) ≤ ENNReal.ofReal ((2 * annulusRadius R i) ^ d)

theorem Algsuperdiff.Section4.Provider.Regularity.lintegral_triadicAnnulus_le {d : ℕ} {x : HCPolySupport.Vec d} {R beta : ℝ} (hR : 0 < R) (hbeta : 0 ≤ beta) (i : ℕ) : ∫⁻ (y : HCPolySupport.Vec d) in triadicAnnulus x R i, ENNReal.ofReal (dist x y ^ (-beta)) ≤ ENNReal.ofReal (annulusTerm d R beta i)

4. The ball estimate

noncomputable def Algsuperdiff.Section4.Provider.Regularity.radialKernelConst (d : ℕ) (beta : ℝ) : ℝ

C_rad(d,β) = 2^d · 3^β · (1 - 3^{β-d})^{-1}, in the closed form the shell sum produces: (R/3)^{-β}(2R)^d divided by 1 - 3^β/3^d, at R = 1.

Equations

• Algsuperdiff.Section4.Provider.Regularity.radialKernelConst d beta = (1 / 3) ^ (-beta) * 2 ^ d / (1 - Algsuperdiff.Section4.Provider.Regularity.annulusRatio d beta)

theorem Algsuperdiff.Section4.Provider.Regularity.one_sub_annulusRatio_pos {d : ℕ} {beta : ℝ} (hbd : beta < ↑d) : 0 < 1 - annulusRatio d beta

theorem Algsuperdiff.Section4.Provider.Regularity.radialKernelConst_pos {d : ℕ} {beta : ℝ} (hbd : beta < ↑d) : 0 < radialKernelConst d beta

theorem Algsuperdiff.Section4.Provider.Regularity.annulusTerm_zero {d : ℕ} {R : ℝ} (hR : 0 < R) (beta : ℝ) : annulusTerm d R beta 0 = R ^ (-beta) * (1 / 3) ^ (-beta) * (2 ^ d * R ^ d)

T_0 = (R/3)^{-β} (2R)^d = C_rad(d,β)·(1 - ratio)·R^{d}·R^{-β}, in the factored form used by the sum.

theorem Algsuperdiff.Section4.Provider.Regularity.lintegral_ball_dist_rpow_neg_le {d : ℕ} {x : HCPolySupport.Vec d} {R beta : ℝ} (hR : 0 < R) (hbeta : 0 < beta) (hbd : beta < ↑d) : ∫⁻ (y : HCPolySupport.Vec d) in Metric.ball x R, ENNReal.ofReal (dist x y ^ (-beta)) ≤ ENNReal.ofReal (radialKernelConst d beta * (R ^ d * R ^ (-beta)))

The radial kernel integral on a ball.

For 0 < β < d, in the ambient supremum metric, ∫_{B(x,R)} |x-y|^{-β} dy ≤ C_rad(d,β) · R^{d} · R^{-β}.

5. The ℝ≥0∞-native form

theorem Algsuperdiff.Section4.Provider.Regularity.volume_singleton_eq_zero {d : ℕ} (hd : 1 ≤ d) (x : HCPolySupport.Vec d) : MeasureTheory.volume {x} = 0

Points are null in Vec d once d ≥ 1 ({x} is the closed ball of radius 0, of volume (2·0)^d).

theorem Algsuperdiff.Section4.Provider.Regularity.lintegral_enorm_sub_rpow_neg_le_of_subset_ball {d : ℕ} {x : HCPolySupport.Vec d} {R beta : ℝ} {A : Set (HCPolySupport.Vec d)} (hA : A ⊆ Metric.ball x R) (hR : 0 < R) (hbeta : 0 < beta) (hbd : beta < ↑d) : ∫⁻ (y : HCPolySupport.Vec d) in A, ‖x - y‖ₑ ^ (-beta) ≤ ENNReal.ofReal (radialKernelConst d beta * (R ^ d * R ^ (-beta)))

The radial kernel integral, with the ℝ≥0∞-native kernel ‖x-y‖ₑ^{-β}.

The two kernels differ only on the diagonal — where the real junk value is 0^{-β} = 0 and the ℝ≥0∞ value is ⊤ — which is null because 0 < β < d forces 1 ≤ d.