Add odd-dimensional iterated norm Laplacian by Lemmy00 · Pull Request #1175 · leanprover-community/physlib

Lemmy00 · 2026-06-12T15:11:44Z

This builds on the norm-power Laplacian and fundamental-solution API added in the preceding PRs.

It adds the odd-dimensional analytic core in a dedicated module: in dimension 2 * m + 1, the (m + 1)-fold distributional Laplacian of the distribution induced by ‖x‖ is an explicit nonzero scalar multiple of diracDelta ℝ 0.

Main additions:

Physlib.SpaceAndTime.Space.Norm.IteratedLaplacian
oddNormIteratedLaplacianCoeff and oddNormIteratedLaplacianCoeff_ne_zero
iterated_distLaplacian_norm_zpow_odd_eq_smul_diracDelta

Verification run locally:

lake build Physlib.SpaceAndTime.Space.Norm Physlib.SpaceAndTime.Space.Norm.IteratedLaplacian
./scripts/lint-style.sh
lake exe runPhyslibLinters
lake build

github-actions · 2026-06-12T15:12:16Z

Thank you for this PR, which will now be reviewed. Please
see our review guidelines
if you are not familiar with the process. You should expect a back and forth
with a reviewer before your PR is merged. See also that link for how to
add appropriate labels to your PR. The PR will also go through a number
of automated checks. You can learn more about these here,
including how to run them locally.

If you want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.

jstoobysmith · 2026-06-12T18:29:51Z

+    (((1 : ℤ) - 2 * (m : ℤ) : ℝ) * (2 * m + 1 : ℝ) *
+      (volume (α := Space (2 * m + 1))).real (Metric.ball 0 1))
+
+private lemma odd_unit_ball_volume_real_pos (m : ℕ) :


This should be moved to the general Integrals file.

jstoobysmith · 2026-06-12T18:30:31Z

+
+This file proves an odd-dimensional iterated-Laplacian identity for the distribution induced by
+the norm on `Space (2 * m + 1)`.
+


Can you write what this corresponds to here.

jstoobysmith · 2026-06-12T18:31:34Z

+
+/-- The scalar factor produced by one nonsingular Laplacian step in dimension `2 * m + 1`,
+after `k` previous Laplacian steps. -/
+noncomputable def oddNormLaplacianStepCoeff (m k : ℕ) : ℝ :=


Do we actually need to make this definition?

Lemmy00 · 2026-06-13T12:21:27Z

Thanks, addressed these in 0e55af4f.

moved the odd unit-ball volume positivity lemma to Space/Integrals/Basic;
expanded the file overview to say this corresponds to the odd-dimensional identity where applying the Laplacian m + 1 times to the norm gives a nonzero constant multiple of δ₀;
removed the separate step-coefficient definition and inlined the factor in the product.

I also reran the local targeted builds, full lake build, style script, Lean linters, and git diff --check.

jstoobysmith · 2026-06-13T22:30:36Z

@@ -397,6 +397,7 @@ public import Physlib.SpaceAndTime.Space.IsDistBounded
 public import Physlib.SpaceAndTime.Space.LengthUnit
 public import Physlib.SpaceAndTime.Space.Module
 public import Physlib.SpaceAndTime.Space.Norm


can we move this ordinary Norm file to Norm.Basic

Done, moved the ordinary Norm file to Norm/Basic and updated the imports.

jstoobysmith

Great! Approved - many thanks.

zhikaip · 2026-06-15T17:52:36Z

see comments below

zhikaip · 2026-06-15T17:53:24Z

 lemma volume_eq_addHaar {d} : (volume (α := Space d)) = Space.basis.toBasis.addHaar := by
  exact (OrthonormalBasis.addHaar_eq_volume _).symm

+lemma volume_closedBall_ne_zero {d : ℕ} (x : Space d.succ) {r : ℝ} (hr : 0 < r) :


I removed volume_closedBall_ne_zero and volume_closedBall_ne_top in #1183, duplicate from Mathlib lemmas

zhikaip · 2026-06-15T17:56:03Z

+    rfl
+
+/-- The real volume of the unit ball in odd-dimensional space is positive. -/
+lemma volume_metricBall_odd_real_pos (m : ℕ) :


this holds for all d, and I think this is simple enough that it doesn't really warrant it's own lemma (Edit: unless this is reused multiple times?):

lemma volume_metricBall_real_pos {d : ℕ}: 0 < (volume (α := Space d)).real (Metric.ball 0 1) := ENNReal.toReal_pos (Metric.measure_ball_pos volume 0 one_pos).ne' measure_ball_lt_top.ne

Done, removed the duplicate closed-ball lemmas and inlined the general unit-ball real-volume positivity proof at the only use site.

Many thanks for this!

Lemmy00 force-pushed the milikic/odd-dimensional-laplacian-core branch 2 times, most recently from 34e158d to 9486f22 Compare June 12, 2026 17:14

jstoobysmith reviewed Jun 12, 2026

View reviewed changes

jstoobysmith added the awaiting-author A reviewer has asked the author a question or requested changes label Jun 12, 2026

Lemmy00 force-pushed the milikic/odd-dimensional-laplacian-core branch from 9486f22 to 0e55af4 Compare June 13, 2026 11:58

jstoobysmith reviewed Jun 13, 2026

View reviewed changes

Add odd-dimensional iterated norm Laplacian

45ab64d

Lemmy00 force-pushed the milikic/odd-dimensional-laplacian-core branch from 0e55af4 to 45ab64d Compare June 14, 2026 04:42

jstoobysmith approved these changes Jun 14, 2026

View reviewed changes

jstoobysmith added ready-to-merge This PR is approved and will be merged shortly and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 14, 2026

Merge branch 'master' into milikic/odd-dimensional-laplacian-core

e8cb886

zhikaip reviewed Jun 15, 2026

View reviewed changes

Address final odd Laplacian review comments

3b30f88

zhikaip merged commit 0403fb0 into leanprover-community:master Jun 15, 2026
9 checks passed


		This file proves an odd-dimensional iterated-Laplacian identity for the distribution induced by
		the norm on `Space (2 * m + 1)`.

Conversation

Lemmy00 commented Jun 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jun 12, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Lemmy00 commented Jun 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jstoobysmith left a comment

Choose a reason for hiding this comment

Uh oh!

zhikaip commented Jun 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

zhikaip Jun 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Lemmy00 commented Jun 12, 2026 •

edited

Loading

Lemmy00 commented Jun 13, 2026 •

edited

Loading

zhikaip commented Jun 15, 2026 •

edited

Loading

zhikaip Jun 15, 2026 •

edited

Loading