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

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.