Repository navigation

refactor: adopt Tau Ceti's good rate functions and large deviation principle - #360

Open

RemyDegenne wants to merge 4 commits into

LeanMachineLearning:mainfrom

RemyDegenne:overlap/342-ldp

Open

refactor: adopt Tau Ceti's good rate functions and large deviation principle#360
RemyDegenne wants to merge 4 commits into
LeanMachineLearning:mainfrom
RemyDegenne:overlap/342-ldp

Commits on Nov 13, 2026
- refactor: adopt Tau Ceti's good rate functions and large deviation principle
  
  RemyDegenne
  and
  claude
  committed
  4acb9d4
- refactor: export the EReal inverse-multiplication lemma from a general file
  
  RemyDegenne
  and
  web-flow
  committed
  5c5d0f9
- refactor: state the EReal inverse-multiplication lemma for every real
  
  RemyDegenne
  and
  web-flow
  committed
  dbac84d
- refactor: name the speed `1 / n` conversion in one EReal lemma
  
  RemyDegenne
  and
  web-flow
  committed
  de1fa53