feat(ProbabilisticTheory): channels and weights - #1670

Open

TomOleDiem wants to merge 31 commits into

leanprover-community:masterfrom

TomOleDiem:probabilistic-theory-weight

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

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

TomOleDiem
and
claude
committed
1ac2235
feat(ProbabilisticTheory): channels and weights

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

TomOleDiem
and
claude
committed
537c283
refactor(ProbabilisticTheory): clean up Weight/Channel API per review

TomOleDiem
and
claude
committed
98bdcb1
fix(ProbabilisticTheory): update for PosCone.exists_real_shift_nonneg rename

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

TomOleDiem
and
claude
committed
f465cd3
docs(Weight): fix meta-commentary docstring on toFun_neg

TomOleDiem
and
claude
committed
8009986
refactor(Weight): drop private on rawValue_of_le/rawValue_indep

TomOleDiem
and
claude
committed
222f336
refactor(Weight): golf mono via direct rw instead of a calc block

TomOleDiem
and
claude
committed
ae77fb5