Physlib.SpaceAndTime.Space.Norm.IteratedLaplacian

Physlib
SpaceAndTime
Space
Norm
IteratedLaplacian

Imports

/-
Copyright (c) 2026 Lazar Milikic. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Lazar Milikic
-/
module

public import Physlib.SpaceAndTime.Space.Norm.Basic

Iterated Laplacians of norm distributions

i. Overview

This file proves the distributional identity corresponding to the classical odd-dimensional formula that, in dimension 2 * m + 1, applying the Laplacian m + 1 times to the norm gives a nonzero constant multiple of the Dirac delta at the origin.

ii. Key results

iterated_distLaplacian_norm_zpow_odd_eq_smul_diracDelta : The (m + 1)-fold Laplacian of the norm in dimension 2 * m + 1 is a nonzero multiple of the Dirac delta.

iii. Table of contents

A. The odd-dimensional iterated Laplacian of the norm

iv. References

@[expose] public section

A. The odd-dimensional iterated Laplacian of the norm



private lemma oddNormIteratedLaplacianCoeff_factor_ne_zero {m k : ℕ} (hk : k < m) :
    ((((1 : ℤ) - 2 * (k : ℤ) : ℤ) : ℝ) *
      ((((1 : ℤ) - 2 * (k : ℤ) - 2 + (2 * m + 1 : ℤ) : ℤ) : ℝ))) ≠ 0 := bym:ℕk:ℕhk:k < m⊢ ↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + (2 * ↑m + 1)) ≠ 0
  apply mul_ne_zeroham:ℕk:ℕhk:k < m⊢ ↑(1 - 2 * ↑k) ≠ 0hbm:ℕk:ℕhk:k < m⊢ ↑(1 - 2 * ↑k - 2 + (2 * ↑m + 1)) ≠ 0
  ·ham:ℕk:ℕhk:k < m⊢ ↑(1 - 2 * ↑k) ≠ 0 have h : (1 : ℤ) - 2 * (k : ℤ) ≠ 0 := bym:ℕk:ℕhk:k < m⊢ ↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + (2 * ↑m + 1)) ≠ 0ham:ℕk:ℕhk:k < mh:1 - 2 * ↑k ≠ 0⊢ ↑(1 - 2 * ↑k) ≠ 0 omegaham:ℕk:ℕhk:k < mh:1 - 2 * ↑k ≠ 0⊢ ↑(1 - 2 * ↑k) ≠ 0ham:ℕk:ℕhk:k < mh:1 - 2 * ↑k ≠ 0⊢ ↑(1 - 2 * ↑k) ≠ 0
    exact_mod_cast hAll goals completed! 🐙
  ·hbm:ℕk:ℕhk:k < m⊢ ↑(1 - 2 * ↑k - 2 + (2 * ↑m + 1)) ≠ 0 have h : (1 : ℤ) - 2 * (k : ℤ) - 2 + (2 * m + 1 : ℤ) ≠ 0 := bym:ℕk:ℕhk:k < m⊢ ↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + (2 * ↑m + 1)) ≠ 0hbm:ℕk:ℕhk:k < mh:1 - 2 * ↑k - 2 + (2 * ↑m + 1) ≠ 0⊢ ↑(1 - 2 * ↑k - 2 + (2 * ↑m + 1)) ≠ 0 omegahbm:ℕk:ℕhk:k < mh:1 - 2 * ↑k - 2 + (2 * ↑m + 1) ≠ 0⊢ ↑(1 - 2 * ↑k - 2 + (2 * ↑m + 1)) ≠ 0hbm:ℕk:ℕhk:k < mh:1 - 2 * ↑k - 2 + (2 * ↑m + 1) ≠ 0⊢ ↑(1 - 2 * ↑k - 2 + (2 * ↑m + 1)) ≠ 0
    exact_mod_cast hAll goals completed! 🐙

The scalar factor in the odd-dimensional iterated Laplacian of the norm is nonzero.


lemma oddNormIteratedLaplacianCoeff_ne_zero (m : ℕ) :
    oddNormIteratedLaplacianCoeff m ≠ 0 := bym:ℕ⊢ oddNormIteratedLaplacianCoeff m ≠ 0
  unfold oddNormIteratedLaplacianCoeffm:ℕ⊢ (∏ k ∈ Finset.range m, ↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + (2 * ↑m + 1))) *
    ((↑1 - 2 * ↑↑m) * (2 * ↑m + 1) * volume.real (Metric.ball 0 1)) ≠
  0
  apply mul_ne_zeroham:ℕ⊢ ∏ k ∈ Finset.range m, ↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + (2 * ↑m + 1)) ≠ 0hbm:ℕ⊢ (↑1 - 2 * ↑↑m) * (2 * ↑m + 1) * volume.real (Metric.ball 0 1) ≠ 0
  ·ham:ℕ⊢ ∏ k ∈ Finset.range m, ↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + (2 * ↑m + 1)) ≠ 0 rw [Finset.prod_ne_zero_iffham:ℕ⊢ ∀ a ∈ Finset.range m, ↑(1 - 2 * ↑a) * ↑(1 - 2 * ↑a - 2 + (2 * ↑m + 1)) ≠ 0ham:ℕ⊢ ∀ a ∈ Finset.range m, ↑(1 - 2 * ↑a) * ↑(1 - 2 * ↑a - 2 + (2 * ↑m + 1)) ≠ 0]ham:ℕ⊢ ∀ a ∈ Finset.range m, ↑(1 - 2 * ↑a) * ↑(1 - 2 * ↑a - 2 + (2 * ↑m + 1)) ≠ 0
    intro k hkham:ℕk:ℕhk:k ∈ Finset.range m⊢ ↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + (2 * ↑m + 1)) ≠ 0
    exact oddNormIteratedLaplacianCoeff_factor_ne_zero (bym:ℕk:ℕhk:k ∈ Finset.range m⊢ k < m simpa using hkAll goals completed! 🐙)
  ·hbm:ℕ⊢ (↑1 - 2 * ↑↑m) * (2 * ↑m + 1) * volume.real (Metric.ball 0 1) ≠ 0 repeat' apply mul_ne_zerohbm:ℕ⊢ volume.real (Metric.ball 0 1) ≠ 0
    ·hb.ha.ham:ℕ⊢ ↑1 - 2 * ↑↑m ≠ 0 have h : (1 : ℤ) - 2 * (m : ℤ) ≠ 0 := bym:ℕ⊢ oddNormIteratedLaplacianCoeff m ≠ 0hb.ha.ham:ℕh:1 - 2 * ↑m ≠ 0⊢ ↑1 - 2 * ↑↑m ≠ 0 omegahb.ha.ham:ℕh:1 - 2 * ↑m ≠ 0⊢ ↑1 - 2 * ↑↑m ≠ 0hb.ha.ham:ℕh:1 - 2 * ↑m ≠ 0⊢ ↑1 - 2 * ↑↑m ≠ 0
      exact_mod_cast hAll goals completed! 🐙
    ·hbm:ℕ⊢ 2 * ↑m + 1 ≠ 0 exact_mod_cast (bym:ℕ⊢ 2 * m + 1 ≠ 0 omegaAll goals completed! 🐙 : (2 * m + 1 : ℕ) ≠ 0)
    ·hbm:ℕ⊢ volume.real (Metric.ball 0 1) ≠ 0 exact ne_of_gt <| ENNReal.toReal_pos
        (Metric.measure_ball_pos volume 0 one_pos).ne'
        measure_ball_lt_top.neAll goals completed! 🐙



private lemma distLaplacian_norm_zpow_odd_boundary (m : ℕ) :
    Δᵈ (distOfFunction (fun x : Space (2 * m + 1) =>
      ‖x‖ ^ ((1 : ℤ) - 2 * (m : ℤ)))
      (IsDistBounded.pow _ (bym:ℕ⊢ -↑(2 * m + 1 - 1) ≤ 1 - 2 * ↑m omegaAll goals completed! 🐙))) =
      (((1 : ℤ) - 2 * (m : ℤ) : ℝ) * (2 * m + 1 : ℝ) *
        (volume (α := Space (2 * m + 1))).real (Metric.ball 0 1)) •
          diracDelta ℝ 0 := bym:ℕ⊢ Δᵈ (distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑m)) ⋯) =
  ((↑1 - 2 * ↑↑m) * (2 * ↑m + 1) * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0
  rcases m with _ | mzero⊢ Δᵈ (distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑0)) ⋯) =
  ((↑1 - 2 * ↑↑0) * (2 * ↑0 + 1) * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0succm:ℕ⊢ Δᵈ (distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(m + 1))) ⋯) =
  ((↑1 - 2 * ↑↑(m + 1)) * (2 * ↑(m + 1) + 1) * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0
  ·zero⊢ Δᵈ (distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑0)) ⋯) =
  ((↑1 - 2 * ↑↑0) * (2 * ↑0 + 1) * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0 rw [distLaplacianzero⊢ (distDiv ∘ₗ ∇ᵈ) (distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑0)) ⋯) =
  ((↑1 - 2 * ↑↑0) * (2 * ↑0 + 1) * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0zero⊢ (distDiv ∘ₗ ∇ᵈ) (distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑0)) ⋯) =
  ((↑1 - 2 * ↑↑0) * (2 * ↑0 + 1) * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0]zero⊢ (distDiv ∘ₗ ∇ᵈ) (distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑0)) ⋯) =
  ((↑1 - 2 * ↑↑0) * (2 * ↑0 + 1) * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0
    change ∇ᵈ ⬝ (∇ᵈ (distOfFunction (fun x : Space 1 => ‖x‖ ^ (1 : ℤ))
      (IsDistBounded.pow 1 (by⊢ -↑(1 - 1) ≤ 1 omegaAll goals completed! 🐙)))) = _
    rw [distGrad_distOfFunction_norm_zpow 1 (by⊢ -↑(1 - 1) + 1 ≤ 1zero⊢ distDiv (distOfFunction (fun x => (↑1 * ‖x‖ ^ (1 - 2)) • basis.repr x) ⋯) =
  ((↑1 - 2 * ↑↑0) * (2 * ↑0 + 1) * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0 omegaAll goals completed! 🐙zero⊢ distDiv (distOfFunction (fun x => (↑1 * ‖x‖ ^ (1 - 2)) • basis.repr x) ⋯) =
  ((↑1 - 2 * ↑↑0) * (2 * ↑0 + 1) * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0)]zero⊢ distDiv (distOfFunction (fun x => (↑1 * ‖x‖ ^ (1 - 2)) • basis.repr x) ⋯) =
  ((↑1 - 2 * ↑↑0) * (2 * ↑0 + 1) * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0
    simp only [Int.cast_one, one_mul]zero⊢ distDiv (distOfFunction (fun x => ‖x‖ ^ (1 - 2) • basis.repr x) ⋯) =
  ((1 - 2 * ↑↑0) * (2 * ↑0 + 1) * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0
    convert! distDiv_inv_pow_eq_dim (d := 1) using 1e'_3⊢ ((1 - 2 * ↑↑0) * (2 * ↑0 + 1) * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0 =
  (↑1 * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0
    ·e'_3⊢ ((1 - 2 * ↑↑0) * (2 * ↑0 + 1) * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0 =
  (↑1 * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0 ext xe'_3x:𝓢(Space (2 * 0 + 1), ℝ)⊢ (((1 - 2 * ↑↑0) * (2 * ↑0 + 1) * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0) x =
  ((↑1 * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0) x
      ring_nfAll goals completed! 🐙
  ·succm:ℕ⊢ Δᵈ (distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(m + 1))) ⋯) =
  ((↑1 - 2 * ↑↑(m + 1)) * (2 * ↑(m + 1) + 1) * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0 convert! distLaplacian_fundamentalSolution_norm_zpow
      (d := 2 * m.succ + 1) using 4e'_2m:ℕx✝:Space (2 * (m + 1) + 1)⊢ ‖x✝‖ ^ (1 - 2 * ↑(m + 1)) = ‖x✝‖ ^ (-(↑(2 * m.succ + 1) - 2))e'_3.e'_5m:ℕ⊢ ↑1 - 2 * ↑↑(m + 1) = -(↑(2 * m.succ + 1) - 2)e'_3.e'_6m:ℕ⊢ 2 * ↑(m + 1) + 1 = ↑(2 * m.succ + 1)
    ·e'_2m:ℕx✝:Space (2 * (m + 1) + 1)⊢ ‖x✝‖ ^ (1 - 2 * ↑(m + 1)) = ‖x✝‖ ^ (-(↑(2 * m.succ + 1) - 2)) simpe'_2m:ℕx✝:Space (2 * (m + 1) + 1)⊢ ‖x✝‖ ^ (1 - 2 * (↑m + 1)) = ‖x✝‖ ^ (2 - (2 * (↑m + 1) + 1)); ring_nfAll goals completed! 🐙
    ·e'_3.e'_5m:ℕ⊢ ↑1 - 2 * ↑↑(m + 1) = -(↑(2 * m.succ + 1) - 2) simpe'_3.e'_5m:ℕ⊢ 1 - 2 * (↑m + 1) = 2 - (2 * (↑m + 1) + 1); ringAll goals completed! 🐙
    ·e'_3.e'_6m:ℕ⊢ 2 * ↑(m + 1) + 1 = ↑(2 * m.succ + 1) simpAll goals completed! 🐙



private lemma iterated_distLaplacian_norm_zpow_odd_until_boundary
    (m k : ℕ) (hk : k ≤ m) :
    ((distLaplacian (d := 2 * m + 1))^[k])
      (distOfFunction (fun x : Space (2 * m + 1) => ‖x‖ ^ (1 : ℤ))
        (IsDistBounded.pow 1 (bym:ℕk:ℕhk:k ≤ m⊢ -↑(2 * m + 1 - 1) ≤ 1 omegaAll goals completed! 🐙))) =
      (∏ j ∈ Finset.range k,
          ((((1 : ℤ) - 2 * (j : ℤ) : ℤ) : ℝ) *
            ((((1 : ℤ) - 2 * (j : ℤ) - 2 + (2 * m + 1 : ℤ) : ℤ) : ℝ)))) •
        distOfFunction (fun x : Space (2 * m + 1) => ‖x‖ ^ ((1 : ℤ) - 2 * (k : ℤ)))
          (IsDistBounded.pow _ (bym:ℕk:ℕhk:k ≤ m⊢ -↑(2 * m + 1 - 1) ≤ 1 - 2 * ↑k omegaAll goals completed! 🐙)) := bym:ℕk:ℕhk:k ≤ m⊢ (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
  (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯
  induction k with
  | zero =>zerom:ℕhk:0 ≤ m⊢ (⇑Δᵈ)^[0] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
  (∏ j ∈ Finset.range 0, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑0)) ⋯
      simpAll goals completed! 🐙
  | succ k ih =>succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ m⊢ (⇑Δᵈ)^[k + 1] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯
      have hk_le : k ≤ m := Nat.le_of_succ_le hksuccm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ (⇑Δᵈ)^[k + 1] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯
      rw [Function.iterate_succ_apply'succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ Δᵈ ((⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯)) =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ Δᵈ ((⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯)) =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯]succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ Δᵈ ((⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯)) =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯
      rw [ih hk_lesuccm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ Δᵈ
    ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯) =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ Δᵈ
    ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯) =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯]succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ Δᵈ
    ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯) =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯
      rw [map_smulsuccm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    Δᵈ (distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯) =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    Δᵈ (distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯) =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯]succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    Δᵈ (distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯) =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯
      rw [distLaplacian_distOfFunction_norm_zpow
        (d := 2 * m + 1) ((1 : ℤ) - 2 * (k : ℤ)) (bym:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ 0 < 1 - 2 * ↑k - 2 + ↑(2 * m + 1)succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1))) • distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯ omegaAll goals completed! 🐙succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1))) • distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯)]succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1))) • distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯
      rw [smul_smulsuccm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯]succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯
      have hdist :
          distOfFunction
              (fun x : Space (2 * m + 1) => ‖x‖ ^ ((1 : ℤ) - 2 * (k : ℤ) - 2))
              (IsDistBounded.pow _ (bym:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ -↑(2 * m + 1 - 1) ≤ 1 - 2 * ↑k - 2succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhdist:distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯ omegaAll goals completed! 🐙succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhdist:distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯)) =
            distOfFunction
              (fun x : Space (2 * m + 1) => ‖x‖ ^ ((1 : ℤ) - 2 * ((k + 1 : ℕ) : ℤ)))
              (IsDistBounded.pow _ (bym:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ -↑(2 * m + 1 - 1) ≤ 1 - 2 * ↑(k + 1)succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhdist:distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯ omegaAll goals completed! 🐙succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhdist:distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯)) := bym:ℕk:ℕhk:k ≤ m⊢ (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
  (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhdist:distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯
        have hexp :
            ((1 : ℤ) - 2 * (k : ℤ) - 2) =
              ((1 : ℤ) - 2 * ((k + 1 : ℕ) : ℤ)) := bym:ℕk:ℕhk:k ≤ m⊢ (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
  (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯m:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhexp:1 - 2 * ↑k - 2 = 1 - 2 * ↑(k + 1)⊢ distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhdist:distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯
          norm_numm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ m⊢ 1 - 2 * ↑k - 2 = 1 - 2 * (↑k + 1)m:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhexp:1 - 2 * ↑k - 2 = 1 - 2 * ↑(k + 1)⊢ distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhdist:distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯
          ringm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhexp:1 - 2 * ↑k - 2 = 1 - 2 * ↑(k + 1)⊢ distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhdist:distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯m:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhexp:1 - 2 * ↑k - 2 = 1 - 2 * ↑(k + 1)⊢ distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhdist:distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯
        ext ηm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhexp:1 - 2 * ↑k - 2 = 1 - 2 * ↑(k + 1)η:𝓢(Space (2 * m + 1), ℝ)⊢ (distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯) η = (distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯) ηsuccm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhdist:distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯
        simp [distOfFunction_apply, hexp]succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhdist:distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhdist:distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯
      rw [hdistsuccm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhdist:distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhdist:distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯]succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhdist:distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯ =
  (∏ j ∈ Finset.range (k + 1), ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯
      rw [Finset.prod_range_succsuccm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhdist:distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯ =
  ((∏ x ∈ Finset.range k, ↑(1 - 2 * ↑x) * ↑(1 - 2 * ↑x - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + (2 * ↑m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhdist:distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯ =
  ((∏ x ∈ Finset.range k, ↑(1 - 2 * ↑x) * ↑(1 - 2 * ↑x - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + (2 * ↑m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯]succm:ℕk:ℕih:∀ (hk : k ≤ m),
  (⇑Δᵈ)^[k] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) =
    (∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k)) ⋯hk:k + 1 ≤ mhk_le:k ≤ mhdist:distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑k - 2)) ⋯ = distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯⊢ ((∏ j ∈ Finset.range k, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + ↑(2 * m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯ =
  ((∏ x ∈ Finset.range k, ↑(1 - 2 * ↑x) * ↑(1 - 2 * ↑x - 2 + (2 * ↑m + 1))) *
      (↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + (2 * ↑m + 1)))) •
    distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑(k + 1))) ⋯
      congr 1All goals completed! 🐙

In dimension 2 * m + 1, the (m + 1)-fold distributional Laplacian of the distribution induced by the norm is a nonzero multiple of the Dirac delta at the origin.


lemma iterated_distLaplacian_norm_zpow_odd_eq_smul_diracDelta (m : ℕ) :
    ((distLaplacian (d := 2 * m + 1))^[m + 1])
      (distOfFunction (fun x : Space (2 * m + 1) => ‖x‖ ^ (1 : ℤ))
        (IsDistBounded.pow 1 (bym:ℕ⊢ -↑(2 * m + 1 - 1) ≤ 1 omegaAll goals completed! 🐙))) =
      oddNormIteratedLaplacianCoeff m • diracDelta ℝ 0 := bym:ℕ⊢ (⇑Δᵈ)^[m + 1] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) = oddNormIteratedLaplacianCoeff m • diracDelta ℝ 0
  rw [Function.iterate_succ_apply'm:ℕ⊢ Δᵈ ((⇑Δᵈ)^[m] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯)) = oddNormIteratedLaplacianCoeff m • diracDelta ℝ 0m:ℕ⊢ Δᵈ ((⇑Δᵈ)^[m] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯)) = oddNormIteratedLaplacianCoeff m • diracDelta ℝ 0]m:ℕ⊢ Δᵈ ((⇑Δᵈ)^[m] (distOfFunction (fun x => ‖x‖ ^ 1) ⋯)) = oddNormIteratedLaplacianCoeff m • diracDelta ℝ 0
  rw [iterated_distLaplacian_norm_zpow_odd_until_boundary m m le_rflm:ℕ⊢ Δᵈ
    ((∏ j ∈ Finset.range m, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑m)) ⋯) =
  oddNormIteratedLaplacianCoeff m • diracDelta ℝ 0m:ℕ⊢ Δᵈ
    ((∏ j ∈ Finset.range m, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑m)) ⋯) =
  oddNormIteratedLaplacianCoeff m • diracDelta ℝ 0]m:ℕ⊢ Δᵈ
    ((∏ j ∈ Finset.range m, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
      distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑m)) ⋯) =
  oddNormIteratedLaplacianCoeff m • diracDelta ℝ 0
  rw [map_smulm:ℕ⊢ (∏ j ∈ Finset.range m, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    Δᵈ (distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑m)) ⋯) =
  oddNormIteratedLaplacianCoeff m • diracDelta ℝ 0m:ℕ⊢ (∏ j ∈ Finset.range m, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    Δᵈ (distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑m)) ⋯) =
  oddNormIteratedLaplacianCoeff m • diracDelta ℝ 0]m:ℕ⊢ (∏ j ∈ Finset.range m, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    Δᵈ (distOfFunction (fun x => ‖x‖ ^ (1 - 2 * ↑m)) ⋯) =
  oddNormIteratedLaplacianCoeff m • diracDelta ℝ 0
  rw [distLaplacian_norm_zpow_odd_boundary mm:ℕ⊢ (∏ j ∈ Finset.range m, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    ((↑1 - 2 * ↑↑m) * (2 * ↑m + 1) * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0 =
  oddNormIteratedLaplacianCoeff m • diracDelta ℝ 0m:ℕ⊢ (∏ j ∈ Finset.range m, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    ((↑1 - 2 * ↑↑m) * (2 * ↑m + 1) * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0 =
  oddNormIteratedLaplacianCoeff m • diracDelta ℝ 0]m:ℕ⊢ (∏ j ∈ Finset.range m, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) •
    ((↑1 - 2 * ↑↑m) * (2 * ↑m + 1) * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0 =
  oddNormIteratedLaplacianCoeff m • diracDelta ℝ 0
  rw [smul_smulm:ℕ⊢ ((∏ j ∈ Finset.range m, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      ((↑1 - 2 * ↑↑m) * (2 * ↑m + 1) * volume.real (Metric.ball 0 1))) •
    diracDelta ℝ 0 =
  oddNormIteratedLaplacianCoeff m • diracDelta ℝ 0m:ℕ⊢ ((∏ j ∈ Finset.range m, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      ((↑1 - 2 * ↑↑m) * (2 * ↑m + 1) * volume.real (Metric.ball 0 1))) •
    diracDelta ℝ 0 =
  oddNormIteratedLaplacianCoeff m • diracDelta ℝ 0]m:ℕ⊢ ((∏ j ∈ Finset.range m, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      ((↑1 - 2 * ↑↑m) * (2 * ↑m + 1) * volume.real (Metric.ball 0 1))) •
    diracDelta ℝ 0 =
  oddNormIteratedLaplacianCoeff m • diracDelta ℝ 0
  unfold oddNormIteratedLaplacianCoeffm:ℕ⊢ ((∏ j ∈ Finset.range m, ↑(1 - 2 * ↑j) * ↑(1 - 2 * ↑j - 2 + (2 * ↑m + 1))) *
      ((↑1 - 2 * ↑↑m) * (2 * ↑m + 1) * volume.real (Metric.ball 0 1))) •
    diracDelta ℝ 0 =
  ((∏ k ∈ Finset.range m, ↑(1 - 2 * ↑k) * ↑(1 - 2 * ↑k - 2 + (2 * ↑m + 1))) *
      ((↑1 - 2 * ↑↑m) * (2 * ↑m + 1) * volume.real (Metric.ball 0 1))) •
    diracDelta ℝ 0
  rflAll goals completed! 🐙