feat(ProbabilisticTheory): states - #1671
TomOleDiem wants to merge 12 commits into
Conversation
…ibAlpha (work-in-progress)
Ladder Operators & Harmonic Oscillator
# Conflicts: # PhyslibAlpha/Mathematics/LadderSystem/Basic.lean # PhyslibAlpha/Mathematics/LadderSystem/Irreducibility.lean # PhyslibAlpha/Mathematics/LadderSystem/OccupationBasis.lean # PhyslibAlpha/Mathematics/LadderSystem/SymmetricPower.lean # PhyslibAlpha/Mathematics/LadderSystem/Vacuum.lean # PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Basic.lean # PhyslibAlpha/QuantumMechanics/HarmonicOscillator/LadderOperators.lean # PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Vacuum.lean
Adds the order-unit foundation for a general probabilistic theory: IsOrderUnit/IsOrderUnitElement (OrderUnit/Basic.lean), the positive cone and its order-unit-shift lemma (OrderUnit/Cone.lean), and the Archimedean order-unit norm with its induced normed-space structure and order-closed topology (OrderUnit/Archimedean.lean). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
|
Thank you for this pull-request (PR). If this is your first PR, welcome to the community! Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.
Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages. If you have any problems or questions, please reach out to the community on the Zulip. |
- IsOrderUnitElement is now a class with named fields (nonneg, exists_nsmul_le) instead of a def unfolding to an And, per review. - ArchimedeanOrderUnitSpace.closedIciTopology is now an instance (was a lemma) so it's found by typeclass search once the order-unit-norm NormedAddCommGroup is installed locally via letI. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Adds effects (Effect/Basic.lean, the sub-unit interval of E), their convex/affine structure and metric (Effect/Convex.lean, Effect/Metric.lean), complementation (Effect/Complement.lean), and sharp effects (Effect/Sharp.lean), building on the order-unit foundation from leanprover-community#1667. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…ic overview Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Effect/{Basic,Complement,Convex,Metric,Sharp}.lean used the granular
pre-review typeclass bundle (AddCommGroup + PartialOrder +
IsOrderedAddMonoid + Module + PosSMulMono + One + IsOrderUnit) and the
old IsOrderUnit/IsArchimedeanOrderUnit names. Switch to the merged
OrderedVectorSpace/OrderUnitSpace/ArchimedeanOrderUnitSpace classes,
dropping the omit-tag dance that the granular version needed.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Adds Channel/Basic.lean (UnitalPositiveLinearMap, a positive linear map preserving the order unit -- the Heisenberg-picture notion of a physical channel) and Weight/Basic.lean + Weight/Extension.lean (extended-nonnegative-real weights on the positive cone, which generalize states by dropping normalization and finiteness, plus the unique linear extension of a finite weight off the cone). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…itSpace API
Weight/{Basic,Extension}.lean used the granular pre-review typeclass
bundle and PosCone.unit, which no longer exist (PosCone now has a
One instance instead). Switch to OrderedVectorSpace/OrderUnitSpace
and (1 : PosCone E).
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Adds the core theory of states: State/Basic.lean (states as unital positive linear functionals, 𝓢[𝕜, A]), State/Convex.lean (mixing of states, pure vs. mixed), State/Metric.lean (the operator-norm distance between states and distance to the nearest pure state), and State/Discrimination.lean (state discrimination, the Helstrom bound, and the equal-prior specialization via state distance). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
State/{Discrimination,Metric}.lean used the granular pre-review
typeclass bundle and old IsOrderUnit/IsArchimedeanOrderUnit names.
Switch to OrderUnitSpace/ArchimedeanOrderUnitSpace, properly scoping
the OrderUnitSpace-only lemmas into their own section in
Discrimination.lean to avoid an instance diamond with the inner
ArchimedeanOrderUnitSpace section.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
a36b8cb to
241cb18
Compare
This branch has not been deployed
2 participants
Summary
Depends on #1667 (order-unit spaces), #1668 (effects), and #1670 (channels and weights) — please review those first.
State/Basic.lean:𝓢[𝕜, A]notation for states — unital positive linear functionals on an ordered vector space with a distinguished unit.State/Convex.lean: mixing of states as a convex combination, pure vs. mixed states.State/Metric.lean: the operator-norm distance between states induced by the order-unit norm, and a state's distance to the nearest pure state.State/Discrimination.lean: the success probability and advantage of guessing between two states, the Helstrom bound.