Repository navigation
Stone's Theorem + Vacuum Definition - #42
Merged
Merged
Conversation
…(stage 1) User additions: item 4 of prpstn:convergence-facts, lmm:self-adjoint-maximally- symmetric, def:hall-10.5 and the new §10.4 Stone's Theorem. Revised after review for formalization: def:spectral-measure and lmm:functional-calculus-bounded; the generator defined on the punctured limit with lmm:generator-spec; def:exp-unitary-group; the long proofs of 10.14, 10.17, 10.18 and 10.15 split into small lemmas; 10.18 rebuilt on Mathlib convolution; Mathlib \lean lists for the imported results. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Shift Lean docstring section references (10.4-10.7 to 10.5-10.8). Rename the home-page section pages, add a §10.4 Stone page and the new §10.3 items, and regenerate item numbers, pages, navigation and counts from the rebuilt blueprint. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…erator Prove that a self-adjoint operator has no proper symmetric extension, name the spectral measure supplied by the unbounded spectral theorem, define the functional calculus f(A), and show it is the bounded integral for bounded f. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Define one-parameter unitary groups, strong continuity and the infinitesimal generator, and prove the easy Stone's theorem lemmas: continuity at zero, the adjoint U(t)* = U(-t), the generator's characterisation and symmetry, the scalar ODE y' = cy, and differentiability of orbits through the generator's domain. Link the imported Mathlib results. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Define e^{itA} from the spectral measure and prove it is a strongly continuous
one-parameter unitary group whose infinitesimal generator is A (Hall 10.14),
with the supporting lemmas: unitarity, the group law, subtraction in the
functional calculus, the difference-quotient norm identity and the derivative
at zero.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… defined Average orbits against smooth compactly supported weights, write the averages as convolutions, and use Mathlib's convolution calculus to show they lie in the generator's domain and approximate every vector (Hall 10.18). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Show the generator of a strongly continuous one-parameter unitary group is
essentially self-adjoint, that the group agrees with e^{itA^cl} on a dense
domain, and conclude that the generator is self-adjoint with U(t) = e^{itA},
uniquely (Hall 10.15).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Factor the dominated-convergence step, the exponential bounds and the difference-quotient norm identity into small helpers, cutting the three long proofs in Exponential.lean to under ten lines each. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Mark the §10.3 functional-calculus nodes and all of §10.4 as formalised, name their Lean declarations, and update the counts, status notes and the guide's table of Lean locations. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Add positivity of unbounded operators, generator lemmas for the trivial, conjugated and bounded-exponential groups, and split the positive-energy API into separate lemmas; restate positive energy through the generator now that Stone's theorem is available, and drop the scaffold wording. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Define positivity of unbounded operators and restate IsPositiveEnergy as a strongly continuous one-parameter unitary group with positive generator. State the generator lemmas for the trivial, conjugated and bounded-exponential groups and the positive-energy API; proofs follow. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Prove positivity of bounded operators and its invariance under unitary conjugation, the generators of the trivial, conjugated and bounded-exponential groups, and the positive-energy lemmas, including the exponential form via Stone's theorem. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Describe the vacuum and ground-state definitions in terms of positive energy with an unbounded generator, and remove the Restriction lines that waited on Stone's theorem. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Renumber items after the new blueprint nodes, add the positivity, generator and positive-energy entries, update titles, counts and section overviews, and replace the restriction note with the completed result. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
On the deployed site the relative links blueprint/... were rewritten to the root-relative /blueprint/..., dropping the /physicslib4 project prefix and returning 404. Point every item link at the full blueprint URL. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.