Is Dist Bounded norm Power Series zpow

@[fun_prop]lemma IsDistBounded.normPowerSeries_zpow {d : ℕ} {n : ℕ} (m : ℤ) :    IsDistBounded (d := d) (fun x => (normPowerSeries n x) ^ m) := by  match m with  | .ofNat m =>    simp only [Int.ofNat_eq_natCast, zpow_natCast]    apply IsDistBounded.mono (f := fun (x : Space d) => (‖x‖ + 1) ^ m)    · fun_prop    · fun_prop    intro x    simp only [norm_pow, Real.norm_eq_abs]    refine pow_le_pow_left₀ (by positivity) ?_ m    rw [abs_of_nonneg (by simp),abs_of_nonneg (by positivity)]    exact normPowerSeries_le_norm_sq_add_one n x  | .negSucc m =>    simp only [zpow_negSucc]    apply IsDistBounded.mono (f := fun (x : Space d) => ((√(1/(n + 1)) : ℝ) ^ (m + 1))⁻¹)    · fun_prop    · exact (((normPowerSeries_differentiable n).continuous.pow _).inv₀        fun x => pow_ne_zero _ (normPowerSeries_ne_zero n x)).aestronglyMeasurable    · intro x      simp only [norm_inv, norm_pow, Real.norm_eq_abs, one_div]      refine inv_anti₀ (by positivity) (pow_le_pow_left₀ (abs_nonneg _) ?_ _)      rw [abs_of_nonneg (by positivity), abs_of_nonneg (by simp), normPowerSeries_eq]      exact Real.sqrt_le_sqrt (by simp)