feat(ProbabilisticTheory): order-unit spaces - #1667

Open

TomOleDiem wants to merge 20 commits into

leanprover-community:masterfrom

TomOleDiem:probabilistic-theory-order-unit

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