Bridge Physlib distributions to tempered distributions

[Lemmy00]

This PR adds a small bridge from Physlib's distribution API to Mathlib's TemperedDistribution API.

Context from previous PRs:

• feat(Space): add radial norm-power divergence formula #1143: radial norm-power divergence formula.
• feat(Space): add distributional Laplacian for norm powers #1169: distributional Laplacian for norm powers.
• feat(Space): add all-dimensional fundamental solution theorem #1172: all-dimensional fundamental solution theorem.
• Add odd-dimensional iterated norm Laplacian #1175: odd-dimensional iterated norm Laplacian.
• Add distributions associated to finite measures #1333: finite-measure distributions in Physlib.

Added in Physlib/Mathematics/Distribution/Basic.lean:

• Distribution.toTemperedDistribution: converts a Physlib distribution to a Mathlib tempered distribution with the pointwise convergence topology.
• Distribution.toTemperedDistribution_apply: evaluation of this conversion is definitionally the original Physlib distribution action.
• Distribution.toTemperedDistribution_fourierTransform: the conversion commutes with the Fourier transform.
• Distribution.toTemperedDistribution_ofFiniteMeasure: the converted Physlib finite-measure distribution agrees with Mathlib's Measure.toTemperedDistribution.

No definitions or lemmas are removed.

Reviewer map:

1. Check the new subsection D.1. Bridge to Mathlib tempered distributions.
2. Check the finite-measure compatibility lemma in subsection E.2, which builds directly on Add distributions associated to finite measures #1333.
3. Check the import replacement from SchwartzSpace.Fourier/PointwiseConvergenceCLM to TemperedDistribution.

Validation run locally:

• lake exe cache get
• lake build Physlib.Mathematics.Distribution.Basic
• lake build
• lake exe lint_all
• ./scripts/lint-style.sh

Notes: the full build prints an existing unused-simp warning in Physlib/Electromagnetism/Kinematics/EMPotential.lean; lake exe lint_all exits successfully while printing existing project-wide advisory style/transitive-import reports outside this PR.

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, 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 are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

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

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

[jstoobysmith]

Looks good for now - I think the key point here is that this only works for complex distributions (as far as I am aware), so we can't utilize Mathlib's distributions fully.

[jstoobysmith]

@Lemmy00 Just saw this was a draft, won't merge it until you say it is ready

[Lemmy00]

@jstoobysmith Yes, that is my understanding too. This bridge is intentionally only for the complex-linear part of the Physlib distribution API, since Mathlib’s 𝓢' is defined using complex Schwartz test functions. The real-valued Physlib distribution API is still needed; this PR just exposes compatibility with Mathlib’s tempered-distribution/Fourier API in the complex setting.