Skip to content

feat(Space): add fundamental solution Laplacian theorem#1171

Merged
jstoobysmith merged 1 commit into
leanprover-community:masterfrom
Lemmy00:lm/dist-laplacian-fundamental-solution
Jun 11, 2026
Merged

feat(Space): add fundamental solution Laplacian theorem#1171
jstoobysmith merged 1 commit into
leanprover-community:masterfrom
Lemmy00:lm/dist-laplacian-fundamental-solution

Conversation

@Lemmy00

@Lemmy00 Lemmy00 commented Jun 11, 2026

Copy link
Copy Markdown
Contributor

This is a follow-up to #1143 and #1169.

It adds the critical norm-power theorem for the distributional Laplacian in dimensions at least three:

Space.distLaplacian_fundamentalSolution_norm_zpow

The proof reuses the existing norm-power gradient theorem and the distDiv_inv_pow_eq_dim Dirac-delta divergence theorem, so this PR does not add new integration infrastructure or refactor the spherical-coordinate API.

Verification:

  • lake env lean Physlib/SpaceAndTime/Space/Norm.lean
  • lake build Physlib.SpaceAndTime.Space.Norm
  • lake build Physlib
  • lake exe runPhyslibLinters
  • ./scripts/lint-style.py Physlib/SpaceAndTime/Space/Norm.lean
  • git diff --check

@github-actions

Copy link
Copy Markdown
Contributor

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 jstoobysmith left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good - approved.

@jstoobysmith jstoobysmith added the ready-to-merge This PR is approved and will be merged shortly label Jun 11, 2026
@jstoobysmith jstoobysmith merged commit 59d11a0 into leanprover-community:master Jun 11, 2026
7 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR is approved and will be merged shortly

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants