OAI/Probability/SKBarriers/Dynamics/FiniteMarkovPath.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SK.Analytic.FiniteMarkov.sum_cons line 14
  2. def OAI.SK.Analytic.FiniteMarkov.walkWeight line 24
  3. theorem OAI.SK.Analytic.FiniteMarkov.walkWeight_zero line 28
  4. theorem OAI.SK.Analytic.FiniteMarkov.walkWeight_cons line 31
  5. theorem OAI.SK.Analytic.FiniteMarkov.walkWeight_nonneg line 34
  6. theorem OAI.SK.Analytic.FiniteMarkov.walkWeight_sum line 40
  7. def OAI.SK.Analytic.FiniteMarkov.pathWeight line 49
  8. theorem OAI.SK.Analytic.FiniteMarkov.pathWeight_nonneg line 52
  9. theorem OAI.SK.Analytic.FiniteMarkov.pathWeight_sum line 56
  10. theorem OAI.SK.Analytic.FiniteMarkov.pathWeight_first line 62
  11. theorem OAI.SK.Analytic.FiniteMarkov.pathWeight_marginal line 69
  12. theorem OAI.SK.Analytic.FiniteMarkov.walkWeight_pos_step line 95
  13. theorem OAI.SK.Analytic.FiniteMarkov.pathWeight_pos_step line 107
  14. def OAI.SK.Analytic.stationaryPathWeight line 118
  15. theorem OAI.SK.Analytic.stationaryPathWeight_sum line 121
  16. theorem OAI.SK.Analytic.stationaryPathWeight_marginal line 125
  17. theorem OAI.SK.Analytic.stationaryPathWeight_pos_jump line 130