Norm Regularized Pow has Temperate Growth

lemma normRegularizedPow_hasTemperateGrowth (d : ℕ) (ε : ℝˣ) (s : ℝ) :    HasTemperateGrowth (normRegularizedPow d ε s) := by  let f1 := fun (x : ℝ) ↦ (ε ^ 2) ^ (s / 2) * x  let f2 := fun (x : Space d) ↦ (1 + ‖x‖ ^ 2) ^ (s / 2)  let f3 := fun (x : Space d) ↦ ε.1⁻¹ • x  have h123 : normRegularizedPow d ε s = f1 ∘ f2 ∘ f3 := by    ext    simp only [normRegularizedPow, f1, f2, f3, comp_apply, norm_smul, norm_inv, Real.norm_eq_abs]    rw [← Real.mul_rpow (sq_nonneg ↑ε) (add_nonneg (zero_le_one' _) (sq_nonneg _))]    simp [mul_add, mul_pow, add_comm]  rw [h123]  fun_prop