OAI/Probability/SKBarriers/Dynamics/PathEndpoint.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SK.Analytic.walkWeight_last line 13
  2. theorem OAI.SK.Analytic.pathFiniteLaw_joint line 30
  3. theorem OAI.SK.Analytic.FiniteLaw.prob_mono_on_support line 39
  4. def OAI.SK.Analytic.extendPath line 53
  5. theorem OAI.SK.Analytic.extendPath_at line 56
  6. theorem OAI.SK.Analytic.extendPath_jump line 59
  7. theorem OAI.SK.Analytic.pathFiniteLaw_visit line 66
  8. def OAI.SK.Analytic.initialBankReference line 73
  9. theorem OAI.SK.Analytic.initialBankReference_path line 77
  10. theorem OAI.SK.Analytic.stationary_sign_crossing_bound line 81