Integrable mul inv pow

lemma integrable_mul_inv_pow {d : ℕ}    {f : Space d → F} (hf : IsDistBounded f) :    ∃ r, Integrable (fun x => ‖((1 + ‖x‖) ^ r)⁻¹‖ • f x) volume := by  suffices h0 : ∀ pmax, ∃ r, ∀ (p : ℤ) (hp : - (d - 1 : ℕ) ≤ p) (c : Space d)      (p_le : p ≤ pmax),      Integrable (fun x => ‖((1 + ‖x‖) ^ r)⁻¹‖ * ‖x + c‖ ^ p) volume by    obtain ⟨n, c, g, p, c_nonneg, p_bound, bound⟩ := hf.2    match n with    | 0 => simp at bound; simp [bound]    | n + 1 =>    let pMax := Finset.max' (Finset.image p Finset.univ) (by simp)    have pMax_max (i : Fin n.succ) : p i ≤ pMax :=      Finset.le_max' _ _ (Finset.mem_image_of_mem p (Finset.mem_univ i))    obtain ⟨r, hr⟩ := h0 pMax    use r    apply Integrable.mono (g := fun x => ∑ i, (c i * (‖((1 + ‖x‖) ^ r)⁻¹‖ * ‖x + g i‖ ^ p i))) _    · fun_prop    · filter_upwards with x      rw [norm_smul]      refine (mul_le_mul_of_nonneg_left (bound x) (by positivity)).trans (le_of_eq ?_)      simp only [norm_inv, norm_pow, Real.norm_eq_abs, abs_abs]      rw [Finset.abs_sum_of_nonneg (fun i _ => mul_nonneg (c_nonneg i) (by positivity)),        Finset.mul_sum]      ring_nf    · refine MeasureTheory.integrable_finsetSum _ fun i _ => Integrable.const_mul ?_ _      refine (hr (p i) (p_bound i) (g i) (pMax_max i)).mono (by fun_prop) ?_      filter_upwards with x      simp  match d with  | 0 => simp  | d + 1 =>  suffices h0 : ∀ (q : ℕ) (c : Space (d + 1)), Integrable (fun x => ‖x + c‖ ^ (q - d : ℤ)        * ‖((1 + ‖x‖) ^ (q + (radialAngularMeasure (d := d + 1)).integrablePower))⁻¹‖) volume by    intro pMax    use (pMax + d).toNat + (radialAngularMeasure (d := d + 1)).integrablePower    intro p hp c p_le    refine (h0 (p + d).toNat c).mono (by fun_prop) ?_    filter_upwards with x    simp only [norm_inv, norm_pow, Real.norm_eq_abs, norm_mul, abs_abs, norm_zpow,      Int.ofNat_toNat]    rw [mul_comm]    refine mul_le_mul ?_ ?_ (by positivity) (by positivity)    · rw [max_eq_left (by omega)]      simp    · refine inv_pow_le_inv_pow_of_le ?_ ?_      · rw [abs_of_nonneg (by positivity)]        simp      · simp_all  let m := (radialAngularMeasure (d := (d + 1))).integrablePower  suffices h0 : ∀ (q : ℕ) (c : Space (d + 1)),      Integrable (fun x => ‖x‖ ^ (q - d : ℤ) * ‖((1 + ‖x - c‖) ^ (q + m))⁻¹‖) volume by    intro q c    convert (h0 q c).comp_add_right c using 1    funext x    simp [m]  suffices h0 : ∀ (q : ℕ) (v : Space (d + 1)),      Integrable (fun x => ‖x‖ ^ q * ‖((1 + ‖x - v‖) ^ (q + m))⁻¹‖) radialAngularMeasure by    intro q v    specialize h0 q v    rw [integrable_radialAngularMeasure_iff] at h0    refine h0.congr (Filter.eventuallyEq_of_mem (compl_mem_ae_iff.mpr (measure_singleton 0))      fun x hx => ?_)    simp [← mul_assoc]    left    rw [zpow_sub₀ (by simpa using hx), zpow_natCast, zpow_natCast]    field_simp  intro q v  have hr1 (x : Space (d + 1)) :        ‖((1 + ‖x - v‖) ^ (q + m))⁻¹‖ = ((1 + ‖x - v‖) ^ (q + m))⁻¹ := by      simp only [norm_inv, norm_pow, Real.norm_eq_abs, inv_inj]      rw [abs_of_nonneg (by positivity)]  apply integrable_of_le_of_pow_mul_le (C₁ := 1) (C₂ := (1 + ‖v‖) ^ (q + m))  · intro x    rw [hr1]    exact inv_le_one_of_one_le₀ (one_le_pow₀ (by simp))  · intro x    rw [hr1]    refine mul_inv_le_of_le_mul₀ ?_ (by positivity) ?_    · positivity    change ‖x‖ ^ (q + m) ≤ _    calc ‖x‖ ^ (q + m) ≤ ((1 + ‖v‖) * (1 + ‖x - v‖)) ^ (q + m) := by          refine pow_le_pow_left₀ (norm_nonneg x) ?_ _          nlinarith [norm_le_norm_add_norm_sub' x v, norm_nonneg (x - v), norm_nonneg v]      _ = (1 + ‖v‖) ^ (q + m) * (1 + ‖x - v‖) ^ (q + m) := mul_pow _ _ _  · exact Measurable.aestronglyMeasurable (by fun_prop)