Skip to content

Commit 0e55af4

Browse files
Lemmy00Lemmy00
committed
Add odd-dimensional iterated norm Laplacian
1 parent fb1ba14 commit 0e55af4

3 files changed

Lines changed: 166 additions & 0 deletions

File tree

‎Physlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -397,6 +397,7 @@ public import Physlib.SpaceAndTime.Space.IsDistBounded
397397
public import Physlib.SpaceAndTime.Space.LengthUnit
398398
public import Physlib.SpaceAndTime.Space.Module
399399
public import Physlib.SpaceAndTime.Space.Norm
400+
public import Physlib.SpaceAndTime.Space.Norm.IteratedLaplacian
400401
public import Physlib.SpaceAndTime.Space.Slice
401402
public import Physlib.SpaceAndTime.Space.Translations
402403
public import Physlib.SpaceAndTime.SpaceTime.Basic

‎Physlib/SpaceAndTime/Space/Integrals/Basic.lean‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,16 @@ lemma volume_closedBall_ne_top {d : ℕ} (x : Space d.succ) (r : ℝ) :
7979
apply not_eq_of_beq_eq_false
8080
rfl
8181

82+
/-- The real volume of the unit ball in odd-dimensional space is positive. -/
83+
lemma volume_metricBall_odd_real_pos (m : ℕ) :
84+
0 < (volume (α := Space (2 * m + 1))).real (Metric.ball 0 1) := by
85+
rw [Measure.real]
86+
rw [InnerProductSpace.volume_ball_of_dim_odd (k := m) (by simp [finrank_eq_dim])]
87+
simp only [finrank_eq_dim, ENNReal.ofReal_one, one_pow, one_mul]
88+
rw [ENNReal.toReal_ofReal]
89+
positivity
90+
positivity
91+
8292
@[simp]
8393
lemma volume_metricBall_three :
8494
volume (Metric.ball (0 : Space 3) 1) = ENNReal.ofReal (4 / 3 * Real.pi) := by

‎Physlib/SpaceAndTime/Space/Norm/IteratedLaplacian.lean‎

Lines changed: 155 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,155 @@
1+
/-
2+
Copyright (c) 2026 Lazar Milikic. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Lazar Milikic
5+
-/
6+
module
7+
8+
public import Physlib.SpaceAndTime.Space.Norm
9+
/-!
10+
11+
# Iterated Laplacians of norm distributions
12+
13+
## i. Overview
14+
15+
This file proves the distributional identity corresponding to the classical odd-dimensional
16+
formula that, in dimension `2 * m + 1`, applying the Laplacian `m + 1` times to the norm
17+
gives a nonzero constant multiple of the Dirac delta at the origin.
18+
19+
## ii. Key results
20+
21+
- `iterated_distLaplacian_norm_zpow_odd_eq_smul_diracDelta` : The `(m + 1)`-fold
22+
Laplacian of the norm in dimension `2 * m + 1` is a nonzero multiple of the Dirac delta.
23+
24+
## iii. Table of contents
25+
26+
- A. The odd-dimensional iterated Laplacian of the norm
27+
28+
## iv. References
29+
30+
-/
31+
32+
@[expose] public section
33+
34+
open SchwartzMap NNReal Physlib
35+
noncomputable section
36+
37+
namespace Space
38+
39+
open MeasureTheory
40+
open Distribution
41+
42+
/-!
43+
44+
## A. The odd-dimensional iterated Laplacian of the norm
45+
46+
-/
47+
48+
/-- The scalar factor in the odd-dimensional iterated Laplacian of the norm. -/
49+
noncomputable def oddNormIteratedLaplacianCoeff (m : ℕ) : ℝ :=
50+
(∏ k ∈ Finset.range m,
51+
((((1 : ℤ) - 2 * (k : ℤ) : ℤ) : ℝ) *
52+
((((1 : ℤ) - 2 * (k : ℤ) - 2 + (2 * m + 1 : ℤ) : ℤ) : ℝ)))) *
53+
(((1 : ℤ) - 2 * (m : ℤ) : ℝ) * (2 * m + 1 : ℝ) *
54+
(volume (α := Space (2 * m + 1))).real (Metric.ball 0 1))
55+
56+
private lemma oddNormIteratedLaplacianCoeff_factor_ne_zero {m k : ℕ} (hk : k < m) :
57+
((((1 : ℤ) - 2 * (k : ℤ) : ℤ) : ℝ) *
58+
((((1 : ℤ) - 2 * (k : ℤ) - 2 + (2 * m + 1 : ℤ) : ℤ) : ℝ))) ≠ 0 := by
59+
apply mul_ne_zero
60+
· have h : (1 : ℤ) - 2 * (k : ℤ) ≠ 0 := by omega
61+
exact_mod_cast h
62+
· have h : (1 : ℤ) - 2 * (k : ℤ) - 2 + (2 * m + 1 : ℤ) ≠ 0 := by omega
63+
exact_mod_cast h
64+
65+
/-- The scalar factor in the odd-dimensional iterated Laplacian of the norm is nonzero. -/
66+
lemma oddNormIteratedLaplacianCoeff_ne_zero (m : ℕ) :
67+
oddNormIteratedLaplacianCoeff m ≠ 0 := by
68+
unfold oddNormIteratedLaplacianCoeff
69+
apply mul_ne_zero
70+
· rw [Finset.prod_ne_zero_iff]
71+
intro k hk
72+
exact oddNormIteratedLaplacianCoeff_factor_ne_zero (by simpa using hk)
73+
· repeat' apply mul_ne_zero
74+
· have h : (1 : ℤ) - 2 * (m : ℤ) ≠ 0 := by omega
75+
exact_mod_cast h
76+
· exact_mod_cast (by omega : (2 * m + 1 : ℕ) ≠ 0)
77+
· exact ne_of_gt (volume_metricBall_odd_real_pos m)
78+
79+
private lemma distLaplacian_norm_zpow_odd_boundary (m : ℕ) :
80+
Δᵈ (distOfFunction (fun x : Space (2 * m + 1) =>
81+
‖x‖ ^ ((1 : ℤ) - 2 * (m : ℤ)))
82+
(IsDistBounded.pow _ (by omega))) =
83+
(((1 : ℤ) - 2 * (m : ℤ) : ℝ) * (2 * m + 1 : ℝ) *
84+
(volume (α := Space (2 * m + 1))).real (Metric.ball 0 1)) •
85+
diracDelta ℝ 0 := by
86+
rcases m with _ | m
87+
· rw [distLaplacian]
88+
change ∇ᵈ ⬝ (∇ᵈ (distOfFunction (fun x : Space 1 => ‖x‖ ^ (1 : ℤ))
89+
(IsDistBounded.pow 1 (by omega)))) = _
90+
rw [distGrad_distOfFunction_norm_zpow 1 (by omega)]
91+
simp only [Int.cast_one, one_mul]
92+
convert distDiv_inv_pow_eq_dim (d := 1) using 1
93+
· ext x
94+
ring_nf
95+
· convert distLaplacian_fundamentalSolution_norm_zpow_of_three_le
96+
(d := 2 * m.succ + 1) (by omega) using 4
97+
· simp [Nat.succ_eq_add_one]
98+
ring
99+
· simp [Nat.succ_eq_add_one]
100+
101+
private lemma iterated_distLaplacian_norm_zpow_odd_until_boundary
102+
(m k : ℕ) (hk : k ≤ m) :
103+
((distLaplacian (d := 2 * m + 1))^[k])
104+
(distOfFunction (fun x : Space (2 * m + 1) => ‖x‖ ^ (1 : ℤ))
105+
(IsDistBounded.pow 1 (by omega))) =
106+
(∏ j ∈ Finset.range k,
107+
((((1 : ℤ) - 2 * (j : ℤ) : ℤ) : ℝ) *
108+
((((1 : ℤ) - 2 * (j : ℤ) - 2 + (2 * m + 1 : ℤ) : ℤ) : ℝ)))) •
109+
distOfFunction (fun x : Space (2 * m + 1) => ‖x‖ ^ ((1 : ℤ) - 2 * (k : ℤ)))
110+
(IsDistBounded.pow _ (by omega)) := by
111+
induction k with
112+
| zero =>
113+
simp
114+
| succ k ih =>
115+
have hk_le : k ≤ m := Nat.le_of_succ_le hk
116+
rw [Function.iterate_succ_apply']
117+
rw [ih hk_le]
118+
rw [map_smul]
119+
rw [distLaplacian_distOfFunction_norm_zpow
120+
(d := 2 * m) ((1 : ℤ) - 2 * (k : ℤ)) (by omega) (by omega)]
121+
rw [smul_smul]
122+
have hdist :
123+
distOfFunction
124+
(fun x : Space (2 * m + 1) => ‖x‖ ^ ((1 : ℤ) - 2 * (k : ℤ) - 2))
125+
(IsDistBounded.pow _ (by omega)) =
126+
distOfFunction
127+
(fun x : Space (2 * m + 1) => ‖x‖ ^ ((1 : ℤ) - 2 * ((k + 1 : ℕ) : ℤ)))
128+
(IsDistBounded.pow _ (by omega)) := by
129+
have hexp :
130+
((1 : ℤ) - 2 * (k : ℤ) - 2) =
131+
((1 : ℤ) - 2 * ((k + 1 : ℕ) : ℤ)) := by
132+
norm_num
133+
ring
134+
ext η
135+
simp [distOfFunction_apply, hexp]
136+
rw [hdist]
137+
rw [Finset.prod_range_succ]
138+
congr 1
139+
140+
/-- In dimension `2 * m + 1`, the `(m + 1)`-fold distributional Laplacian of the
141+
distribution induced by the norm is a nonzero multiple of the Dirac delta at the origin. -/
142+
lemma iterated_distLaplacian_norm_zpow_odd_eq_smul_diracDelta (m : ℕ) :
143+
((distLaplacian (d := 2 * m + 1))^[m + 1])
144+
(distOfFunction (fun x : Space (2 * m + 1) => ‖x‖ ^ (1 : ℤ))
145+
(IsDistBounded.pow 1 (by omega))) =
146+
oddNormIteratedLaplacianCoeff m • diracDelta ℝ 0 := by
147+
rw [Function.iterate_succ_apply']
148+
rw [iterated_distLaplacian_norm_zpow_odd_until_boundary m m le_rfl]
149+
rw [map_smul]
150+
rw [distLaplacian_norm_zpow_odd_boundary m]
151+
rw [smul_smul]
152+
unfold oddNormIteratedLaplacianCoeff
153+
rfl
154+
155+
end Space

0 commit comments

Comments
 (0)