Repository navigation

feat: the Bernoulli maximal inequality, counts versus pseudo-counts [DLB17, Lemma F.4] - #292

Merged

lmlexplore-automation[bot] merged 4 commits into

LeanMachineLearning:mainfrom

RemyDegenne:roadmap/bernoulli-maximal-inequality-essakine2026tight-reinforcementlearning

Nov 13, 2026

Merged

feat: the Bernoulli maximal inequality, counts versus pseudo-counts [DLB17, Lemma F.4]#292
lmlexplore-automation[bot] merged 4 commits into
LeanMachineLearning:mainfrom
RemyDegenne:roadmap/bernoulli-maximal-inequality-essakine2026tight-reinforcementlearning

Commits on Nov 12, 2026
- feat: the Bernoulli maximal inequality, counts versus pseudo-counts [DLB17, Lemma F.4]
  
  RemyDegenne
  and
  web-flow
  committed
  2ae57c6
Commits on Nov 13, 2026
- chore: name LMLExplore contributors in the headers of the new files
  
  RemyDegenne
  and
  claude
  committed
  1263b27
- refactor: reuse the [0, 1] chord and integrability lemmas in the Bernoulli maximal bound
  
  RemyDegenne
  and
  web-flow
  committed
  187630d
- refactor: prove the Bernoulli integrability helper from integrable_exp_mul_of_le
  
  RemyDegenne
  and
  web-flow
  committed
  e973ab3