Gradient dist norm Power Series zpow tends To dist Grad norm

lemma gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm {d : ℕ} [NeZero d] (m : ℤ)    (hm : - (d - 1 : ℕ) ≤ m) (η : 𝓢(Space d, ℝ))    (y : EuclideanSpace ℝ (Fin d)) :    Filter.Tendsto (fun n =>    ⟪(∇ᵈ (distOfFunction    (fun x : Space d => (normPowerSeries n x) ^ m) (by fun_prop))) η, y⟫_ℝ)    Filter.atTop    (𝓝 (⟪∇ᵈ (distOfFunction (fun x : Space d => ‖x‖ ^ m)    (IsDistBounded.pow m hm)) η, y⟫_ℝ)) := by  simp only [distGrad_inner_eq, Distribution.fderivD_apply, distOfFunction_apply]  change Filter.Tendsto (fun n => - ∫ (x : Space d),      fderiv ℝ η x (basis.repr.symm y) * normPowerSeries n x ^ m)    Filter.atTop (𝓝 (- ∫ (x : Space d), fderiv ℝ η x (basis.repr.symm y) * ‖x‖ ^ m))  apply Filter.Tendsto.neg  apply MeasureTheory.tendsto_integral_of_dominated_convergence    (bound := fun x => |fderiv ℝ η x (basis.repr.symm y)| * ((‖x‖ + 1) ^ m + ‖x‖ ^ m))  · intro n    exact IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul (F := ℝ) (by fun_prop) η _  · have h1 : Integrable (fun x =>        (fderiv ℝ (⇑η) x) (basis.repr.symm y) * ((‖x‖ + 1) ^ m + ‖x‖ ^ m)) volume := by      apply IsDistBounded.integrable_space_fderiv        ((IsDistBounded.norm_add_pos_nat_zpow m 1 one_pos).add (IsDistBounded.pow m hm))    refine h1.abs.congr (ae_of_all _ fun x => ?_)    simp only [abs_mul]    congr 1    exact abs_of_nonneg (by positivity)  · intro n    filter_upwards [Measure.ae_ne volume 0] with x hx    simp [abs_of_nonneg (normPowerSeries_nonneg n x)]    exact mul_le_mul_of_nonneg_left      (normPowerSeries_zpow_le_norm_sq_add_one n m x hx) (abs_nonneg _)  · filter_upwards [Measure.ae_ne volume 0] with x hx    exact tendsto_const_nhds.mul      ((normPowerSeries_tendsto x hx).zpow₀ m (.inl (norm_ne_zero_iff.mpr hx)))