trajMeasure definition for Mathlib - #24

Merged

RemyDegenne merged 12 commits into

LeanMachineLearning:mainfrom

paulorauber:trajMeasure

Sep 16, 2025

Commits on Sep 15, 2025

Refactor lemmas
paulorauber
committed
774ce01
Merge branch 'main' into trajMeasure
paulorauber
committed
f1e3c0a
Remove redundant content
paulorauber
committed
d0d2960
Ready to start replacing trajMeasure on Bandit.lean
paulorauber
committed
ab60b26

Commits on Sep 16, 2025

Merged with trajMeasure
paulorauber
committed
c910ea6
Fix lint
paulorauber
committed
1deb375
Fix lint
paulorauber
committed
d85c785
Remove redundant results
paulorauber
committed
f01d769
Update LeanBandits/Bandit.lean

paulorauber
and
RemyDegenne
authored
184dd99
Update LeanBandits/Bandit.lean

paulorauber
and
RemyDegenne
authored
93a4cbe
Update LeanBandits/Bandit.lean

paulorauber
and
RemyDegenne
authored
cd6dbfd
Change lemma name
paulorauber
committed
cda4b01