Inverse-distance cutoff integrals

The scalar radial integral is finite and equals twice the square root of the radius.

The radial Jacobian cancels two powers of the inverse-distance power.

theorem LiebThirring.Assembly.lintegral_rpow_neg_half (r : ℝ) (hr : 0 < r) : ∫⁻ (t : ℝ) in Set.Ioo 0 r, ENNReal.ofReal (t ^ (-1 / 2)) = ENNReal.ofReal (2 * √r)

The scalar radial integral is finite and equals twice the square root of the radius.

theorem LiebThirring.Assembly.radial_inv_rpow_integrand (t : ℝ) (ht : 0 < t) : ENNReal.ofReal (t ^ 2) * (ENNReal.ofReal t)⁻¹ ^ (5 / 2) = ENNReal.ofReal (t ^ (-1 / 2))

The radial Jacobian cancels two powers of the inverse-distance power.

theorem LiebThirring.Assembly.lintegral_ball_inv_rpow (r : ℝ) (hr : 0 < r) : ∫⁻ (x : Position), (if ‖x‖ < r then (ENNReal.ofReal ‖x‖)⁻¹ else 0) ^ (5 / 2) = ENNReal.ofReal (8 * Real.pi * √r)

The extended inverse-distance power integrates to 8π√r on the radius cutoff.

noncomputable def LiebThirring.Assembly.nucleusCutoff (a r : ℝ) (z x : Position) : ENNReal

The cutoff of the inverse distance to a single nucleus.

Equations

• LiebThirring.Assembly.nucleusCutoff a r z x = if ‖x - z‖ < r then ENNReal.ofReal a * (ENNReal.ofReal ‖x - z‖)⁻¹ else 0

theorem LiebThirring.Assembly.measurable_nucleusCutoff (a r : ℝ) (z : Position) : Measurable (nucleusCutoff a r z)

One-center cutoffs are measurable, including their infinite value at the center.

theorem LiebThirring.Assembly.lintegral_nucleusCutoff_rpow (a r : ℝ) (ha : 0 ≤ a) (hr : 0 < r) (z : Position) : ∫⁻ (x : Position), nucleusCutoff a r z x ^ (5 / 2) = ENNReal.ofReal (8 * Real.pi * a ^ (5 / 2) * √r)

The exact one-center power integral used to majorize the nearest-nucleus cutoff.