Gradient dist norm Power Series log

lemma gradient_dist_normPowerSeries_log {d : ℕ} {n : ℕ} :    ∇ᵈ (distOfFunction (fun x : Space d => Real.log (normPowerSeries n x)) (by fun_prop)) =    distOfFunction (fun x : Space d => ((normPowerSeries n x) ^ (- 2 : ℤ)) • basis.repr x)    (by fun_prop) := by  ext1 η  refine ext_inner_right ℝ fun y => ?_  simp [distGrad_inner_eq]  rw [Distribution.fderivD_apply, distOfFunction_apply, distOfFunction_inner]  calc _    _ = - ∫ (x : Space d), fderiv ℝ η x (basis.repr.symm y) * Real.log (normPowerSeries n x) := by      rfl    _ = ∫ (x : Space d), η x *        fderiv ℝ (fun x => Real.log (normPowerSeries n x)) x (basis.repr.symm y) := by      rw [integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable]      · fun_prop      · refine IsDistBounded.integrable_space_mul ?_ η        simp only [fderiv_log_normPowerSeries]        fun_prop      · fun_prop      · fun_prop      · exact fun _ _ => Differentiable.differentiableAt (by fun_prop)    _ = ∫ (x : Space d), η x * (⟪basis.repr.symm y, x⟫_ℝ * (normPowerSeries n x) ^ (- 2 : ℤ)) := by      simp only [fderiv_log_normPowerSeries]  congr  funext x  simp [inner_smul_left_eq_smul]  left  rw [real_inner_comm, basis_repr_inner_eq]  ring