Repository navigation

feat: convergence and optional stopping of ℝ≥0∞-valued supermartingales at arbitrary stopping times - #396

Closed

RemyDegenne wants to merge 5 commits into

LeanMachineLearning:mainfrom

RemyDegenne:roadmap/stoppedvaluelimsup-worker1

Closed

feat: convergence and optional stopping of ℝ≥0∞-valued supermartingales at arbitrary stopping times#396
RemyDegenne wants to merge 5 commits into
LeanMachineLearning:mainfrom
RemyDegenne:roadmap/stoppedvaluelimsup-worker1

Commits on Nov 14, 2026
- feat: convergence and optional stopping of ℝ≥0∞-valued supermartingales at arbitrary stopping times
  
  RemyDegenne
  and
  web-flow
  committed
  161f39e
- refactor: move stoppedValueLimsup to Probability/Process, address review
  
  RemyDegenne
  and
  web-flow
  committed
  ec12cfe
- refactor: use a WithTop ℕ helper for n < x → n + 1 ≤ x in optional stopping
  
  RemyDegenne
  and
  web-flow
  committed
  018e769
- refactor: add isStoppingTime_top and use it in optional stopping
  
  RemyDegenne
  and
  web-flow
  committed
  b3de0d2
- refactor: move isStoppingTime_top to Probability/Process/Stopping
  
  RemyDegenne
  and
  web-flow
  committed
  c2ee0ae