Integrable On norm rpow ball compl iff

lemma integrableOn_norm_rpow_ball_compl_iff {d : ℕ} [NeZero d] {a : ℝ} (ha : 0 < a) (p : ℝ) :    IntegrableOn (fun x : Space d ↦ ‖x‖ ^ p) (Metric.ball 0 a)ᶜ ↔ d + p < 0 := by  let f : Space d → ENNReal := (Metric.ball 0 a)ᶜ.indicator (fun x ↦ ‖‖x‖ ^ p‖ₑ)  let g : ℝ → ℝ := (Set.Ici a).indicator (fun r ↦ r ^ p)  have hfg : f = fun x ↦ ‖g ‖x‖‖ₑ := by ext x; by_cases ‖x‖ ∈ Set.Ici a <;> simp_all [f, g]  trans Integrable (fun x : Space d ↦ g ‖x‖)  · refine and_congr ?_ ?_    · refine iff_of_true ?_ ?_      repeat exact StronglyMeasurable.aestronglyMeasurable (by measurability)    · dsimp [HasFiniteIntegral]      rw [← lintegral_indicator (by measurability), lintegral_congr_ae hfg.eventuallyEq]  trans IntegrableOn (fun r => r ^ (d - 1 + p)) (Set.Ici a)  · have hInter : Set.Ici a ∩ Set.Ioi 0 = Set.Ici a := by ext; grind    simp_rw [integrable_fun_norm_addHaar, g, Space.finrank_eq_dim,      npow_indicator_rpow_eq (Set.notMem_Ici.mpr ha),      _root_.MeasureTheory.integrableOn_indicator_iff measurableSet_Ici, hInter,      Nat.cast_pred (Nat.pos_of_neZero d)]  rw [integrableOn_Ici_iff_integrableOn_Ioi, integrableOn_Ioi_rpow_iff ha, lt_neg_iff_add_neg]  ring_nf