Gradient dist norm Power Series log tends To dist Grad norm

lemma gradient_dist_normPowerSeries_log_tendsTo_distGrad_norm {d : ℕ} (hd : 2 ≤ d)    (η : 𝓢(Space d, ℝ)) (y : EuclideanSpace ℝ (Fin d)) :    Filter.Tendsto (fun n =>    ⟪(∇ᵈ (distOfFunction    (fun x : Space d => Real.log (normPowerSeries n x)) (by fun_prop))) η, y⟫_ℝ)    Filter.atTop    (𝓝 (⟪∇ᵈ (distOfFunction (fun x : Space d => Real.log ‖x‖)    (IsDistBounded.log_norm)) η, y⟫_ℝ)) := by  haveI : NeZero d := ⟨by omega⟩  simp only [distGrad_inner_eq, Distribution.fderivD_apply, distOfFunction_apply]  change Filter.Tendsto (fun n => -    ∫ (x : Space d), fderiv ℝ η x (basis.repr.symm y) * Real.log (normPowerSeries n x))    Filter.atTop (𝓝 (- ∫ (x : Space d), fderiv ℝ η x (basis.repr.symm y) * Real.log ‖x‖))  apply Filter.Tendsto.neg  apply MeasureTheory.tendsto_integral_of_dominated_convergence    (bound := fun x => |fderiv ℝ η x (basis.repr.symm y)| * (‖x‖⁻¹ + (‖x‖ + 1)))  · intro n    exact IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul (F := ℝ) (by fun_prop) η _  · have h1 : Integrable (fun x => (fderiv ℝ (⇑η) x) (basis.repr.symm y) *        (‖x‖⁻¹ + (‖x‖ + 1))) volume := by      apply IsDistBounded.integrable_space_fderiv        (IsDistBounded.add IsDistBounded.inv (by fun_prop))    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 only [norm_mul, Real.norm_eq_abs]    exact mul_le_mul_of_nonneg_left (normPowerSeries_log_le n x hx) (abs_nonneg _)  · filter_upwards [Measure.ae_ne volume 0] with x hx    exact tendsto_const_nhds.mul      ((normPowerSeries_tendsto x hx).log (norm_ne_zero_iff.mpr hx))