OAI/Probability/FreeIsing/Estimates/ContinuousOptionalStopping.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.ContinuousOptionalStopping.countable_range_const line 13
  2. theorem OAI.Problem367.ContinuousOptionalStopping.countable_range_min line 19
  3. theorem OAI.Problem367.ContinuousOptionalStopping.integrable_stoppedValue_of_countable line 31
  4. theorem OAI.Problem367.ContinuousOptionalStopping.integral_stoppedValue_of_countable line 38
  5. theorem OAI.Problem367.ContinuousOptionalStopping.martingale_stoppedProcess_of_countable line 46
  6. theorem OAI.Problem367.ContinuousOptionalStopping.martingale_stoppedProcess_of_approximation line 97
  7. theorem OAI.Problem367.ContinuousOptionalStopping.martingale_stoppedProcess_of_approximation_bounded line 138
  8. theorem OAI.Problem367.ContinuousOptionalStopping.martingale_stopped_compensatedSquare_of_approximation line 153
  9. theorem OAI.Problem367.ContinuousOptionalStopping.martingale_stoppedProcess_of_continuous_dominated line 189
  10. theorem OAI.Problem367.ContinuousOptionalStopping.martingale_stoppedProcess_of_continuous_bounded line 199
  11. theorem OAI.Problem367.ContinuousOptionalStopping.martingale_stopped_compensatedSquare line 208