Dist Div inv pow eq dim

lemma distDiv_inv_pow_eq_dim {d : ℕ} [NeZero d] :    ∇ᵈ ⬝ (distOfFunction (fun x : Space d => ‖x‖ ^ (- d : ℤ) • basis.repr x)      (IsDistBounded.zpow_smul_repr_self (- d : ℤ) (by omega))) =      (d * (volume (α := Space d)).real (Metric.ball 0 1)) • diracDelta ℝ 0 := by  ext η  calc _      _ = - ∫ x, ⟪‖x‖⁻¹ ^ d • basis.repr x, Space.grad η x⟫_ℝ := by          simp only [zpow_neg, zpow_natCast, distDiv_ofFunction, inv_pow]      _ = - ∫ x, ‖x‖⁻¹ ^ (d - 1) * ⟪‖x‖⁻¹ • basis.repr x, Space.grad η x⟫_ℝ := by          simp only [← pow_sub_one_mul (NeZero.ne d), inv_pow, inner_smul_left, conj_trivial,            map_inv₀, neg_inj]          ring_nf      _ = - ∫ x, ‖x‖⁻¹ ^ (d - 1) * (_root_.deriv (fun a => η (a • ‖x‖⁻¹ • x)) ‖x‖) := by          simp only [real_inner_comm,            ← grad_inner_space_unit_vector _ _ (SchwartzMap.differentiable η)]      _ = - ∫ r, ‖r.2.1‖⁻¹ ^ (d - 1) * (_root_.deriv (fun a => η (a • r.1)) ‖r.2.1‖)        ∂(volume (α := Space d).toSphere.prod        (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))) := by          rw [← MeasureTheory.MeasurePreserving.integral_comp (f := homeomorphUnitSphereProd _)            (MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd            (volume (α := Space d)))            (Homeomorph.measurableEmbedding (homeomorphUnitSphereProd (Space d)))]          congr 1          simp only [inv_pow, homeomorphUnitSphereProd_apply_snd_coe, norm_norm,            homeomorphUnitSphereProd_apply_fst_coe]          let f (x : Space d) : ℝ :=            (‖↑x‖ ^ (d - 1))⁻¹ * _root_.deriv (fun a => η (a • ‖↑x‖⁻¹ • ↑x)) ‖↑x‖          conv_rhs =>            enter [2, x]            change f x.1          rw [MeasureTheory.integral_subtype_comap (by simp), ← setIntegral_univ]          change ∫ x in Set.univ, f x = ∫ (x : Space d) in _, f x          exact setIntegral_congr_set (MeasureTheory.ae_eq_univ.mpr (by simp)).symm      _ = - ∫ n, (∫ r, ‖r.1‖⁻¹ ^ (d - 1) *        (_root_.deriv (fun a => η (a • n)) ‖r.1‖)        ∂((Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))))        ∂(volume (α := Space d).toSphere) := by          rw [MeasureTheory.integral_prod]          /- Integrable condition. -/          convert integrable_isDistBounded_inner_grad_schwartzMap_spherical            (IsDistBounded.inv_pow_smul_repr_self (d) (by omega)) η          rename_i r          simp only [Real.norm_eq_abs, inv_pow, Function.comp_apply,            homeomorphUnitSphereProd_symm_apply_coe, map_smul]          let x : Space d := r.2.1 • r.1.1          have hr : (0 : ℝ) < r.2.1 := r.2.2          rw [abs_of_nonneg (le_of_lt hr)]          trans (r.2.1 ^ (d - 1))⁻¹ * _root_.deriv (fun a => η (a • ‖↑x‖⁻¹ • ↑x)) ‖x‖          · simp [x, norm_smul]            left            congr            funext a            congr            simp [smul_smul]            rw [abs_of_nonneg (le_of_lt hr)]            field_simp            simp only [one_smul]            rw [abs_of_nonneg (le_of_lt hr)]          rw [← grad_inner_space_unit_vector, real_inner_comm, ← pow_sub_one_mul (NeZero.ne d)]          simp only [norm_smul, Real.norm_eq_abs, abs_of_nonneg (le_of_lt hr),            norm_eq_of_mem_sphere, mul_one, map_smul, inner_smul_left, map_inv₀, conj_trivial,            mul_inv_rev, x]          field_simp          exact SchwartzMap.differentiable η      _ = - ∫ n, (∫ (r : Set.Ioi (0 : ℝ)),        (_root_.deriv (fun a => η (a • n)) r.1) ∂(.comap Subtype.val volume))        ∂(volume (α := Space d).toSphere) := by          congr          funext n          simp [Measure.volumeIoiPow]          erw [integral_withDensity_eq_integral_smul]          congr          funext r          have hr : (0 : ℝ) < r.1 := r.2          rw [abs_of_nonneg hr.le, NNReal.smul_def, Real.coe_toNNReal _ (by positivity),            smul_eq_mul, ← mul_assoc, mul_inv_cancel₀ (pow_ne_zero (d - 1) hr.ne'), one_mul]          fun_prop      _ = - ∫ n, (-η 0) ∂(volume (α := Space d).toSphere) := by          congr          funext n          let η' (n : ↑(Metric.sphere 0 1)) : 𝓢(ℝ, ℝ) := compCLM (g := fun a => a • n.1) ℝ (by            apply And.intro            · fun_prop            · intro n'              match n' with              | 0 =>                use 1, 1                simp [norm_smul]              | 1 =>                use 0, 1                intro x                simp [fderiv_smul_const]              | n' + 1 + 1 =>                use 0, 0                intro x                simp only [Real.norm_eq_abs, pow_zero, mul_one, norm_le_zero_iff]                rw [iteratedFDeriv_succ_eq_comp_right]                conv_lhs =>                  enter [2, 3, y]                  simp [fderiv_smul_const]                rw [iteratedFDeriv_succ_const]                rfl) (by use 1, 1; simp [norm_smul]) η          rw [MeasureTheory.integral_subtype_comap (by simp),            MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto (f := fun a => η (a • n)) (m := 0)]          · simp          · exact ContinuousAt.continuousWithinAt (by fun_prop)          · exact fun x _ => DifferentiableAt.hasDerivAt (by fun_prop)          · exact (integrable ((derivCLM ℝ ℝ) (η' n))).integrableOn          · exact Filter.Tendsto.mono_left (η' n).toZeroAtInfty.zero_at_infty' atTop_le_cocompact      _ = η 0 * (d * (volume (α := Space d)).real (Metric.ball 0 1)) := by          simp only [integral_const, Measure.toSphere_real_apply_univ, finrank_eq_dim, smul_eq_mul,            mul_neg, neg_neg]          ring  simp only [_root_.smul_apply, diracDelta_apply, smul_eq_mul]  ring