Integrable space

@[fun_prop]lemma integrable_space {d : ℕ} {f : Space d → F} (hf : IsDistBounded f)    (η : 𝓢(Space d, ℝ)) :    Integrable (fun x : Space d => η x • f x) volume := by  /- Reducing the problem to `Integrable (fun x : Space d => η x * ‖x + c‖ ^ p)` -/  suffices h2 : ∀ (p : ℤ) (hp : - (d - 1 : ℕ) ≤ p) (c : Space d) (η : 𝓢(Space d, ℝ)),      Integrable (fun x : Space d => η x * ‖x + c‖ ^ p) volume by    obtain ⟨n, c, g, p, c_nonneg, p_bound, bound⟩ := hf.2    apply Integrable.mono (g := fun x => ∑ i, (c i * (‖η x‖ * ‖x + g i‖ ^ p i))) _    · fun_prop    · filter_upwards with x      rw [norm_smul]      refine (mul_le_mul_of_nonneg_left (bound x) (norm_nonneg (η x))).trans (le_of_eq ?_)      simp only [Real.norm_eq_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 ?_ _      simpa using (h2 (p i) (p_bound i) (g i) η).norm  /- Reducing the problem to `Integrable (fun x : Space d => η x * ‖x‖ ^ p)` -/  suffices h0 : ∀ (p : ℤ) (hp : - (d - 1 : ℕ) ≤ p) (η : 𝓢(Space d, ℝ)),      Integrable (fun x : Space d => η x * ‖x‖ ^ p) volume by    intro p hp c η    suffices h1 : Integrable (fun x => η ((x + c) - c) * ‖x + c‖ ^ p) volume by      simpa using h1    apply MeasureTheory.Integrable.comp_add_right (g := c) (f := fun x => η (x - c) * ‖x‖ ^ p)    apply h0 p hp (η.compCLM (𝕜 := ℝ) ?_ ?_)    · apply Function.HasTemperateGrowth.of_fderiv (k := 1) (C := 1 + ‖c‖)      · convert Function.HasTemperateGrowth.const (ContinuousLinearMap.id ℝ (Space d))        simp [fderiv_sub_const]      · fun_prop      · refine fun x => (norm_sub_le _ _).trans (le_of_sub_nonneg ?_)        ring_nf        positivity    · refine ⟨1, (1 + ‖c‖), fun x => (norm_le_norm_add_norm_sub' x c).trans (le_of_sub_nonneg ?_)⟩      ring_nf      positivity  /- Proving `Integrable (fun x : Space d => η x * ‖x + c‖ ^ p)` -/  intro p hp η  rw [← MeasureTheory.integrable_norm_iff (AEMeasurable.aestronglyMeasurable (by fun_prop))]  simp only [norm_mul, norm_zpow, norm_norm]  match d with  | 0 => simp only [Real.norm_eq_abs, Integrable.of_finite]  | d + 1 =>  by_cases hp' : p = 0  · subst hp'    simpa using η.integrable.norm  suffices h1 : Integrable (fun x => ‖η x‖ * ‖x‖ ^ (p + d)) (radialAngularMeasure (d := (d + 1))) by    rw [integrable_radialAngularMeasure_iff] at h1    convert h1 using 1    funext x    generalize ‖x‖ = r    simp only [Real.norm_eq_abs, add_tsub_cancel_right, one_div, smul_eq_mul]    rw [mul_left_comm]    congr 1    by_cases hr : r = 0    · subst hr      simp [zero_pow_eq, zero_zpow_eq, hp']      omega    field_simp    rw [zpow_add₀ hr]    rfl  convert integrable_pow_mul_iteratedFDeriv radialAngularMeasure η (p + d).toNat 0 using 1  funext x  simp only [Real.norm_eq_abs, norm_iteratedFDeriv_zero]  rw [mul_comm, ← zpow_natCast, Int.toNat_of_nonneg (by omega)]