Repository navigation

feat: the self-bounding inequality [MDJKLV21, Lemma 13] with the corrected constant - #287

Merged

lmlexplore-automation[bot] merged 5 commits into

LeanMachineLearning:mainfrom

RemyDegenne:roadmap/self-bounding-inequality-essakine2026tight-reinforcementlearning

Nov 13, 2026

Merged

feat: the self-bounding inequality [MDJKLV21, Lemma 13] with the corrected constant#287
lmlexplore-automation[bot] merged 5 commits into
LeanMachineLearning:mainfrom
RemyDegenne:roadmap/self-bounding-inequality-essakine2026tight-reinforcementlearning

Commits on Nov 12, 2026
- feat: the self-bounding inequality [MDJKLV21, Lemma 13] with the corrected constant
  
  RemyDegenne
  and
  web-flow
  committed
  feedb0d
- fix: address review of the self-bounding inequality
  
  RemyDegenne
  and
  web-flow
  committed
  f7f8e84
Commits on Nov 13, 2026
- chore: name LMLExplore contributors in the headers of the new files
  
  RemyDegenne
  and
  claude
  committed
  d0103f2
- refactor: export one_le_log_mul from Log/Basic
  
  RemyDegenne
  and
  web-flow
  committed
  7cfb604
- doc: attribute the corrected constant to le_of_le_sqrt_mul_add
  
  RemyDegenne
  and
  web-flow
  committed
  280e59e