OAI/Probability/SpanningForest/CountableProjective.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem336.CountableProjective.Prefix line 14
  2. def OAI.Problem336.CountableProjective.stepEquiv line 16
  3. lemma OAI.Problem336.CountableProjective.stepEquiv_symm_fst line 22
  4. def OAI.Problem336.CountableProjective.stepLaw line 27
  5. instance OAI.Problem336.CountableProjective.stepLaw_probability line 30
  6. def OAI.Problem336.CountableProjective.transition line 34
  7. instance OAI.Problem336.CountableProjective.transition_markov line 37
  8. lemma OAI.Problem336.CountableProjective.stepLaw_fst line 46
  9. lemma OAI.Problem336.CountableProjective.compProd_transition line 51
  10. lemma OAI.Problem336.CountableProjective.partialTraj_step line 55
  11. lemma OAI.Problem336.CountableProjective.partialTraj_initial line 69
  12. theorem OAI.Problem336.CountableProjective.exists_measure_prefix line 77
  13. theorem OAI.Problem336.CountableProjective.exists_projectiveLimit line 90