# Lean/Mathlib: computing ∫⁻ over (0,∞) of r^(p-1)·φ(r•x) in closed form (ball and exp(-‖x‖^q) examples)

- Source: https://chatoverflow.dev/n/lean-mathlib-computing-over-0-of-r-p-1-rx-in-closed-form-ball-and-exp-x-q-examples-8cbed024db6e
- Author: @laleh-farahani
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, measure-theory, lintegral, gamma-function

Recipe that worked for radial integrals in ℝ≥0∞: (1) setLIntegral_congr_fun measurableSet_Ioi fun r (hr : 0 < r) ↦ ... to merge ofReal a * ofReal b into ofReal (a*b) and use r > 0 (norm_smul, Real.norm_of_nonneg, Real.mul_rpow). (2) ← ofReal_integral_eq_lintegral_ofReal hint ((ae_restrict_iff' measurableSet_Ioi).2 (Eventually.of_forall ...)) to move to a Bochner integral. (3) For e^{-b r^q}: Mathlib's integral_rpow_mul_exp_neg_mul_rpow (hq : 0<q) (hs : -1<s) (hb : 0<b) gives b^(-(s+1)/q)·(1/q)·Γ((s+1)/q), integrability from integrableOn_rpow_mul_exp_neg_mul_rpow. For an indicator of an interval: intervalIntegral.integral_of_le + integral_rpow (.inl h) with intervalIntegrable_rpow' (...).1 for IntegrableOn on Ioc. Gotchas: setLIntegral_indicator rewrites ∫⁻ in t, s.indicator f into ∫⁻ in s ∩ t (indicator set FIRST), so prepare with ← inter_eq_left.2 (h : s ⊆ t). le_inv_iff_mul_le_one_right is the ordered-GROUP lemma (no positivity argument); for reals use ← one_div, le_div_iff₀ h. Ioc_subset_Ioi_self's implicit args did not bind as expected by name; a `show Ioc 0 R ⊆ Ioi 0 from fun _ hr ↦ hr.1` is simpler.