Integral mul schwartz Map bounded

lemma integral_mul_schwartzMap_bounded {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) :    ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),    0 ≤ C ∧ ∀ (η : 𝓢(Space d, ℝ)),    ‖∫ (x : Space d), η x • f x‖ ≤ C * (s.sup (schwartzSeminormFamily ℝ (Space d) ℝ)) η := by  obtain ⟨r, hr⟩ := hf.integrable_mul_inv_pow  use Finset.Iic (r, 0), 2 ^ r * ∫ x, ‖f x‖ * ‖((1 + ‖x‖) ^ r)⁻¹‖  refine ⟨by positivity, fun η ↦ (norm_integral_le_integral_norm _).trans ?_⟩  rw [← integral_const_mul, ← integral_mul_const]  refine integral_mono_of_nonneg ?_ ?_ ?_  · filter_upwards with x    positivity  · refine (Integrable.congr' hr (AEStronglyMeasurable.mul (by fun_prop)      (AEMeasurable.aestronglyMeasurable (by fun_prop))) ?_).const_mul _ |>.mul_const _    filter_upwards with x    simp [norm_smul, mul_comm]  · filter_upwards with x    simp [norm_smul]    trans (2 ^ r *      ((Finset.Iic (r, 0)).sup (schwartzSeminormFamily ℝ (Space d) ℝ)) η      *(|1 + ‖x‖| ^ r)⁻¹) * ‖f x‖; swap    · apply le_of_eq      ring    apply mul_le_mul_of_nonneg ?_ (by rfl) (by positivity) (by positivity)    have h0 := one_add_le_sup_seminorm_apply (𝕜 := ℝ) (m := (r, 0))      (k := r) (n := 0) le_rfl le_rfl η x    rw [le_mul_inv_iff₀ (by positivity)]    convert! h0 using 1    simp only [norm_iteratedFDeriv_zero, Real.norm_eq_abs]    ring_nf    congr    rw [abs_of_nonneg (by positivity)]