Integrable On norm rpow ball iff

lemma integrableOn_norm_rpow_ball_iff {d : ℕ} [NeZero d] {b : ℝ} (hb : 0 < b) (p : ℝ) :    IntegrableOn (fun x : Space d ↦ ‖x‖ ^ p) (Metric.ball 0 b) ↔ 0 < d + p := by  let f : Space d → ENNReal := (Metric.ball 0 b).indicator (fun x ↦ ‖‖x‖ ^ p‖ₑ)  let g : ℝ → ℝ := (Set.Ioo 0 b).indicator (fun r ↦ r ^ p)  have hfg : f =ᵐ[volume] fun x ↦ ‖g ‖x‖‖ₑ := by    apply ae_iff.mpr    suffices {x | f x ≠ ‖g ‖x‖‖ₑ} = if p = 0 then {0} else ∅ by by_cases p = 0 <;> simp_all    ext x    by_cases ‖x‖ ∈ Set.Ioo 0 b    · simp_all [f, g]    · by_cases x = 0 <;> simp_all [f, g, Real.zero_rpow_eq_iff]  trans Integrable (fun x : Space d ↦ g ‖x‖)  · refine and_congr ?_ ?_    · refine iff_of_true ?_ ?_      repeat exact StronglyMeasurable.aestronglyMeasurable (by measurability)    · rw [HasFiniteIntegral, ← lintegral_indicator measurableSet_ball, lintegral_congr_ae hfg]      rfl  trans IntegrableOn (fun r => r ^ (d - 1 + p)) (Set.Ioo 0 b)  · have hInter : Set.Ioo 0 b ∩ Set.Ioi 0 = Set.Ioo 0 b := by ext; grind    simp_rw [integrable_fun_norm_addHaar, g, Space.finrank_eq_dim,      npow_indicator_rpow_eq (Set.left_notMem_Ioo),      _root_.MeasureTheory.integrableOn_indicator_iff measurableSet_Ioo, hInter,      Nat.cast_pred (Nat.pos_of_neZero d)]  rw [intervalIntegral.integrableOn_Ioo_rpow_iff hb, neg_lt_iff_pos_add']  ring_nf