feat(ProbabilisticTheory): effects - #1668
TomOleDiem wants to merge 11 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>
1ac2e95 to
13a2e08
Compare
[OrderedVectorSpace E] [One E] was repeating identically across four Effect files. Give it its own class, OrderedVectorSpaceWithUnit, and have OrderUnitSpace extend it instead of extending both directly. Purely internal: OrderUnitSpace's public API is unchanged. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
13a2e08 to
642dafb
Compare
Per feedback: prefer using OrderUnitSpace uniformly in Effect files over introducing a new intermediate class for the recurring [OrderedVectorSpace E] [One E] combo. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
642dafb to
cf66884
Compare
…itSpace IsOrderUnitElement was only ever instantiated at A = 1 (as the type of OrderUnitSpace.isOrderUnitElement_one), so the indirection bought nothing. Fold its two fields (nonneg, exists_nsmul_le) directly into OrderUnitSpace as one_nonneg and exists_nsmul_one_le. 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
OrderUnitSpace/ArchimedeanOrderUnitSpace classes uniformly, dropping
the omit-tag dance that the granular version needed.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
cf66884 to
a9d86ab
Compare
This branch has not been deployed
2 participants
Summary
Depends on #1667 (order-unit spaces) — please review that first.
Effect/Basic.lean:Effect E, the sub-unit interval{0 ≤ A ≤ 1}of an order-unit space, i.e. the possible outcomes of a yes/no test.Effect/Convex.lean: convex/affine mixing of effects.Effect/Metric.lean: the order-unit-norm metric on effects.Effect/Complement.lean: the complementary effect1 - e.Effect/Sharp.lean: sharp (projection-like) effects.