feat(ProbabilisticTheory): states - #1671

Open

TomOleDiem wants to merge 34 commits into

leanprover-community:masterfrom

TomOleDiem:probabilistic-theory-state-core

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
2f06dd0
fix(ProbabilisticTheory): drop inline lemma citation from Effect.Metric overview

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

TomOleDiem
and
claude
committed
e836854
feat(ProbabilisticTheory): channels and weights

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

TomOleDiem
and
claude
committed
53097d9
feat(ProbabilisticTheory): states

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

TomOleDiem
and
claude
committed
356f7cd
refactor(ProbabilisticTheory): clean up State core API per review

TomOleDiem
and
claude
committed
f29c5ee
style(ProbabilisticTheory): drop redundant letI now the norm is scoped

TomOleDiem
and
claude
committed
f3e1c43
fix(ProbabilisticTheory): fix remaining stale OrderUnit references

TomOleDiem
and
claude
committed
8634a28
fix(ProbabilisticTheory): sync Weight/Channel with #1670 review cleanup

TomOleDiem
and
claude
committed
2d706d9
refactor(State): factor out repeated Nonempty instance in dist proofs

TomOleDiem
and
claude
committed
9ba028b
refactor(State): drop private on Weight/Extension, Convex, Discrimination lemmas

TomOleDiem
and
claude
committed
f1eb707
refactor(State,Weight): golf advantage_le with nlinarith; sync mono golf

TomOleDiem
and
claude
committed
1da8864