Integrable On norm rpow shell

lemma integrableOn_norm_rpow_shell {d : ℕ} {a : ℝ} (ha : 0 < a) (b p : ℝ) :    IntegrableOn (fun x : Space d ↦ ‖x‖ ^ p) ((Metric.ball 0 b) ∩ (Metric.ball 0 a)ᶜ) := by  refine ⟨StronglyMeasurable.aestronglyMeasurable (by measurability), ?_⟩  by_cases hab : a < b  · refine setLIntegral_lt_top_of_le_nnreal ?_ ?_    · exact measure_inter_ne_top_of_left_ne_top measure_ball_ne_top    · use ‖max (a ^ p) (b ^ p)‖₊      intro x hx      simp only [Set.mem_inter_iff, Metric.mem_ball, dist_zero_right, Set.mem_compl_iff] at hx      rw [enorm_le_coe]      refine abs_le_abs_of_nonneg (Real.rpow_nonneg (norm_nonneg x) p) ?_      rw [le_sup_iff]      by_cases hp : 0 ≤ p      · exact Or.inr <| Real.rpow_le_rpow (norm_nonneg x) (by linarith) hp      · exact Or.inl <| Real.rpow_le_rpow_of_nonpos ha (by linarith) (by linarith)  · suffices (Metric.ball 0 b) ∩ (Metric.ball 0 a)ᶜ = (∅ : Set (Space d)) by simp [this]    ext x    have : ‖x‖ < b → ‖x‖ < a := fun _ ↦ by linarith    simpa