feat(ProbabilisticTheory): effects - #1668

Open

TomOleDiem wants to merge 30 commits into

leanprover-community:masterfrom

TomOleDiem:probabilistic-theory-effects

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

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

TomOleDiem
and
claude
committed
0dbc9df
refactor(ProbabilisticTheory): clean up Effect API per review

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

TomOleDiem
and
claude
committed
33fbfc7
refactor(ProbabilisticTheory): tighten typeclasses and name instances

TomOleDiem
and
claude
committed
92e735e
revert: keep mix/IsSharp under OrderUnitSpace, not bare One

TomOleDiem
and
claude
committed
38912d8
refactor(ProbabilisticTheory): golf exists_pos_smul_mem, split equivBall proofs

TomOleDiem
and
claude
committed
de5f247
fix(ProbabilisticTheory): restore two lemmas dropped by an earlier pass

TomOleDiem
and
claude
committed
6a16c27
style(ProbabilisticTheory): golf several Effect proofs

TomOleDiem
and
claude
committed
fab0d3b