Repository navigation

feat: the randomized Markov inequality and randomized e-to-p calibration - #412

Merged

lmlexplore-automation[bot] merged 2 commits into

LeanMachineLearning:mainfrom

RemyDegenne:roadmap/randomized-markov-worker4

Nov 15, 2026

Merged

feat: the randomized Markov inequality and randomized e-to-p calibration#412
lmlexplore-automation[bot] merged 2 commits into
LeanMachineLearning:mainfrom
RemyDegenne:roadmap/randomized-markov-worker4

Commits on Nov 15, 2026
- feat: the randomized Markov inequality and randomized e-to-p calibration
  
  RemyDegenne
  and
  web-flow
  committed
  475553c
- fix: weaken freezing lemma to AEMeasurable, name ofReal in uniform identity, fix docstring
  
  RemyDegenne
  and
  web-flow
  committed
  2898b3d