feat(QuantumMechanics): Sobolev submodules of SpaceDHilbertSpace#1434
Conversation
|
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 |
gloges
left a comment
gloges
left a comment
There was a problem hiding this comment.
Thanks, the Sobolev results look good! A few minor suggested changes collect them into a SobolevSubmodule namespace. I have more reservations about some of the distribution lemmas and schwartzIncl_apply; please let me know what you think.
@jstoobysmith would you mind having a look at (or suggesting someone else to check) the tempered distribution parts which I am less familiar with? For example, should we be using Physlib.Distribution instead of Mathlib's TemperedDistribution?
gloges
added
the
awaiting-author
|
-awaiting-author |
github-actions
Bot
removed
the
awaiting-author
|
awaiting-author |
github-actions
Bot
added
the
awaiting-author
04e7a66 to
db59f12
Compare
github-actions
Bot
removed
the
awaiting-author
|
Okay, I think this takes care of the mathlib/physlib distribution issue? Happy to change it if there are further edits to make. |
gloges
left a comment
gloges
left a comment
There was a problem hiding this comment.
Two minor suggestions to rehome the tempered distribution stuff (which has wider applicability than just Sobolev spaces), but otherwise looks good to me.
gloges
added
the
awaiting-author
Add Mathematics/Distribution/Tempered.lean with the general API for the embedding Lp → 𝓢': Lp.toTemperedDistribution_injective, the _add/_smul/_zero simp lemmas, and Lp.smulLeftCLM_toTemperedDistribution_eq_iff (for a temperate-growth symbol g, the distributional identity g · φ = u holds iff g • φ =ᵐ u). Add SpaceD/SobolevSubmodule.lean defining sobolevSubmodule d s (H^s as a submodule of SpaceDHilbertSpace d), with Schwartz-map membership, density, and antitonicity in s. Add the schwartzIncl_apply rfl-lemma to SchwartzSubmodule.lean. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Per review: collect the Sobolev lemmas into a SobolevSubmodule namespace and stop breaking out of the SpaceDHilbertSpace abstraction. Add toTemperedDistribution / toTemperedDistributionCLM aliases (E = Space d, F = ℂ, p = 2 fixed, mirroring MemHS) with the bridge lemma SchwartzSubmodule.toTemperedDistribution_schwartzIncl_eq, and remove schwartzIncl_apply. Define the submodule via the CLM so map_* applies, dropping the toTemperedDistribution_add/smul/zero restatements; remove toTemperedDistribution_injective. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Reformat per the style guide.
The Sobolev submodule now rests entirely on Mathlib's Lp and MemSobolev API; the smulLeftCLM lemmas move to the momentum PR where they are used. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
…ion API The tempered-distribution aliases have wider applicability than Sobolev spaces, so they move out of SobolevSubmodule.lean: - `toTemperedDistribution` / `toTemperedDistributionCLM` land in a new section A.5 (Tempered Distribution) of HilbertSpaces/SpaceD/Basic.lean, between A.4 (Coersions) and Misc. (now A.6). - `SchwartzSubmodule.toTemperedDistribution_schwartzIncl_eq` lands in section A of HilbertSpaces/SpaceD/SchwartzSubmodule.lean, dropping an unneeded `[μ.IsOpenPosMeasure]` hypothesis on the way. - SobolevSubmodule.lean keeps only the Sobolev submodule itself; its remaining section renumbers to A and the module docstring is trimmed. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
435ccd7 to
f3a11fa
Compare
|
-awaiting-author |
github-actions
Bot
removed
the
awaiting-author
gloges
left a comment
gloges
left a comment
There was a problem hiding this comment.
Sorry, just a few minor nitpicks to clean things up.
gloges
added
awaiting-author
|
I think I got everything. |
github-actions
Bot
removed
the
awaiting-author
gloges
left a comment
gloges
left a comment
There was a problem hiding this comment.
Looks good - thanks again!
2 participants
Add Mathematics/Distribution/Tempered.lean with the general API for the embedding Lp → 𝓢': Lp.toTemperedDistribution_injective, the _add/_smul/_zero simp lemmas, and Lp.smulLeftCLM_toTemperedDistribution_eq_iff (for a temperate-growth symbol g, the distributional identity g · φ = u holds iff g • φ =ᵐ u).
Add SpaceD/SobolevSubmodule.lean defining sobolevSubmodule d s (H^s as a submodule of SpaceDHilbertSpace d), with Schwartz-map membership, density, and antitonicity in s. Add the schwartzIncl_apply rfl-lemma to SchwartzSubmodule.lean.