feat(ProbabilisticTheory): channels and weights - #1670
TomOleDiem wants to merge 10 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>
2510e4c to
408630c
Compare
This branch has not been deployed
2 participants
Summary
Depends on #1667 (order-unit spaces) and #1668 (effects) — please review those first.
Channel/Basic.lean:UnitalPositiveLinearMap, notatedE →ₚ₁[R] F— a positive linear map preserving the order unit, i.e. the Heisenberg-picture notion of a physical channel.Weight/Basic.lean:Weight E, an extended-nonnegative-real linear functional on the positive cone — generalizes a state by dropping normalization and finiteness.Weight/Extension.lean: the unique linear extension of a finite weight from the positive cone to the whole space (Weight.IsFinite.toLinearMap).