Repository navigation

feat: integrals and conditional expectations against a conditional distribution - #297

Queued

RemyDegenne wants to merge 3 commits into

LeanMachineLearning:mainfrom

RemyDegenne:roadmap/hasconddistrib-integrals-condexp-essakine2026tight-reinforcementlearning

Queued

feat: integrals and conditional expectations against a conditional distribution#297
RemyDegenne wants to merge 3 commits into
LeanMachineLearning:mainfrom
RemyDegenne:roadmap/hasconddistrib-integrals-condexp-essakine2026tight-reinforcementlearning

Commits on Nov 12, 2026
- feat: integrals and conditional expectations against a conditional distribution
  
  RemyDegenne
  and
  web-flow
  committed
  83dc34d
Commits on Nov 13, 2026
- Merge remote-tracking branch 'origin/main' into roadmap/hasconddistrib-integrals-condexp-essakine2026tight-reinforcementlearning
  RemyDegenne
  committed
  ed71545
- refactor: reuse HasLaw lemmas and share the compProd integrability step
  
  RemyDegenne
  and
  web-flow
  committed
  5db0008