Repository navigation

feat: conditional e-variables, test supermartingales and wealth processes - #385

Merged

lmlexplore-automation[bot] merged 4 commits into

LeanMachineLearning:mainfrom

RemyDegenne:roadmap/istestsupermartingale-worker1

Nov 14, 2026

Merged

feat: conditional e-variables, test supermartingales and wealth processes#385
lmlexplore-automation[bot] merged 4 commits into
LeanMachineLearning:mainfrom
RemyDegenne:roadmap/istestsupermartingale-worker1

Commits on Nov 14, 2026
- feat: conditional e-variables, test supermartingales and wealth processes
  
  RemyDegenne
  and
  web-flow
  committed
  5dfd243
- fix: expose the adaptedness of wealth products, tag the constant-one lemmas simp
  
  RemyDegenne
  and
  web-flow
  committed
  1db3b9f
- feat: add IsTestMartingale.measurable
  
  RemyDegenne
  and
  web-flow
  committed
  aa5b9c5
- refactor: bridge conditional e-variables to condLExp, rename the betting pair
  
  RemyDegenne
  and
  web-flow
  committed
  64cf215