Potential Decay Unit Ball

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

Integrability of the inverse-power weight ‖x‖^{-3/2} on three-dimensional space, in the local and unit-ball forms used to dominate the singular pressure kernel P of the Caffarelli–Kohn–Nirenberg paper.

theorem CKN.locallyIntegrable_inv_norm_rpow_three_halves : MeasureTheory.LocallyIntegrable (fun (x : Foundation.Parabolic.Vec3) => ‖x‖ ^ (-(3 / 2))) MeasureTheory.volume

The inverse power ‖x‖^{-3/2} is locally integrable on three-dimensional space.

theorem CKN.lintegral_ball_one_inv_norm_rpow_lt_top : ∫⁻ (x : Foundation.Parabolic.Vec3) in Metric.ball 0 1, ENNReal.ofReal (‖x‖ ^ (-(3 / 2))) < ⊤

Its integral over the unit ball is finite.