Add odd-dimensional iterated norm Laplacian

[Lemmy00]

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]

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]

This should be moved to the general Integrals file.

[jstoobysmith]

Can you write what this corresponds to here.

[jstoobysmith]

Do we actually need to make this definition?

[Lemmy00]

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.