Skip to content

feat(QM): Add LinearPMap.sum#1120

Merged
jstoobysmith merged 9 commits into
leanprover-community:masterfrom
gloges:operator-sums
May 25, 2026
Merged

feat(QM): Add LinearPMap.sum#1120
jstoobysmith merged 9 commits into
leanprover-community:masterfrom
gloges:operator-sums

Conversation

@gloges
Copy link
Copy Markdown
Contributor

@gloges gloges commented May 23, 2026

Adds to the functionality of unbounded operators:

  • Defines LinearPMap.sum for finite sums of partial linear maps. While sum f and ∑ a, f a are equal, it is not by definition and the latter is difficult to work with.
  • Proves that U is densely defined iff U.closure is densely defined, allowing redundant hypotheses to be removed for essentially self-adjoint operators.

@gloges
Copy link
Copy Markdown
Contributor Author

gloges commented May 23, 2026

t-quantum-mechanics

@github-actions github-actions Bot added the t-quantum-mechanics Quantum mechanics label May 23, 2026
Copy link
Copy Markdown
Member

@jstoobysmith jstoobysmith left a comment

Choose a reason for hiding this comment

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

Looks good - approved. will merge shortly.

@jstoobysmith jstoobysmith added the ready-to-merge This PR is approved and will be merged shortly label May 24, 2026
@jstoobysmith jstoobysmith merged commit 085dab8 into leanprover-community:master May 25, 2026
4 checks passed
@gloges gloges deleted the operator-sums branch May 25, 2026 04:11
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 t-quantum-mechanics Quantum mechanics

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants