feat(ProbabilisticTheory): state separation - #1672

Open

TomOleDiem wants to merge 36 commits into

leanprover-community:masterfrom

TomOleDiem:probabilistic-theory-state-pairing

Commits on Aug 15, 2026

Add LadderSystem and HarmonicOscillator experimental modules to PhyslibAlpha (work-in-progress)
TomOleDiem
committed
47b4d33
Merge pull request #1 from TomOleDiem/add-ladder-fock-to-PhyslibAlpha
TomOleDiem
authored
7349a6b

Commits on Sep 17, 2026

Merge remote-tracking branch 'upstream/master'
TomOleDiem
committed
14d12c8

Commits on Sep 20, 2026

feat(ProbabilisticTheory): order-unit spaces

TomOleDiem
and
claude
committed
4f06dd0

Commits on Sep 23, 2026

fix(ProbabilisticTheory): address order-unit PR review comments

TomOleDiem
and
claude
committed
042c65b
refactor(ProbabilisticTheory): factor out OrderedVectorSpaceWithUnit

TomOleDiem
and
claude
committed
5c3cd62
revert(ProbabilisticTheory): drop OrderedVectorSpaceWithUnit

TomOleDiem
and
claude
committed
dc67b36
refactor(ProbabilisticTheory): inline IsOrderUnitElement into OrderUnitSpace

TomOleDiem
and
claude
committed
42e26f9

Commits on Sep 25, 2026

merge: bring in v4.34.1 toolchain bump from master
TomOleDiem
committed
6d33a37
Update Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean

TomOleDiem
and
morrison-daniel
authored
0345d44
Update Physlib/ProbabilisticTheory/OrderUnit/Basic.lean

TomOleDiem
and
morrison-daniel
authored
f152cf2
Update Physlib/ProbabilisticTheory/OrderUnit/Basic.lean

TomOleDiem
and
morrison-daniel
authored
adc2ab2
Update Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean

TomOleDiem
and
morrison-daniel
authored
2d69266
Update Physlib/ProbabilisticTheory/OrderUnit/Cone.lean

TomOleDiem
and
morrison-daniel
authored
2e48f79
Update Physlib/ProbabilisticTheory/OrderUnit/Cone.lean

TomOleDiem
and
morrison-daniel
authored
17ec3a3
Update Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean

TomOleDiem
and
morrison-daniel
authored
8e1eb3a
Update Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean

TomOleDiem
and
morrison-daniel
authored
c0aa828
fix(ProbabilisticTheory): complete review fixes and avoid instance diamond

TomOleDiem
and
claude
committed
10da2c3
style(ProbabilisticTheory): drop qualification on isClosed_Ici_zero

TomOleDiem
and
claude
committed
d8d306a
style(ProbabilisticTheory): finish dropping redundant qualification

TomOleDiem
and
claude
committed
4210c19
feat(ProbabilisticTheory): effects

TomOleDiem
and
claude
committed
8adb327
fix(ProbabilisticTheory): drop inline lemma citation from Effect.Metric overview

TomOleDiem
and
claude
committed
1e8311c
fix(ProbabilisticTheory): update Effect files for the OrderUnitSpace API

TomOleDiem
and
claude
committed
6ceff28
feat(ProbabilisticTheory): channels and weights

TomOleDiem
and
claude
committed
a9a302d
fix(ProbabilisticTheory): update Weight/Channel files for the OrderUnitSpace API

TomOleDiem
and
claude
committed
a097b62
feat(ProbabilisticTheory): states

TomOleDiem
and
claude
committed
e5b8d41
fix(ProbabilisticTheory): update State files for the OrderUnitSpace API

TomOleDiem
and
claude
committed
c8f344e
feat(ProbabilisticTheory): state separation and duality

TomOleDiem
and
claude
committed
c1b9bdf
fix(ProbabilisticTheory): update State files for the OrderUnitSpace API

TomOleDiem
and
claude
committed
f907901
refactor(ProbabilisticTheory): partial State pairing/separation cleanup

TomOleDiem
and
claude
committed
5e71568
fix(ProbabilisticTheory): rebase fixups and finish review cleanup

TomOleDiem
and
claude
committed
34f650d
fix(ProbabilisticTheory): fix remaining stale Effect/Sharp reference

TomOleDiem
and
claude
committed
67343f6
fix(ProbabilisticTheory): sync State.Convex/Discrimination/Metric with #1671 cleanup

TomOleDiem
and
claude
committed
1659eed
fix(ProbabilisticTheory): sync Weight/Channel with #1670 cleanup

TomOleDiem
and
claude
committed
521dfe9
refactor(State): drop private across Weight/Extension, Convex, Discrimination, Separation, Pairing

TomOleDiem
and
claude
committed
6eb0d83
refactor(State,Weight): golf toWeight map_smul'; sync mono/advantage_le golfs

TomOleDiem
and
claude
committed
c1058ac