OAI/Probability/Ballisticity/Stationary/StationaryMarking.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.preserving_cond line 13
  2. lemma OAI.DirectionalTransience.preserving_marking line 21
  3. def OAI.DirectionalTransience.currentClassKernel line 49
  4. instance OAI.DirectionalTransience.currentClassKernel_markov line 51
  5. def OAI.DirectionalTransience.arrayClassKernel line 54
  6. instance OAI.DirectionalTransience.arrayClassKernel_markov line 56
  7. abbrev OAI.DirectionalTransience.MarkedArray line 59
  8. def OAI.DirectionalTransience.markedShift line 60
  9. lemma OAI.DirectionalTransience.markedShift_measurable line 62
  10. def OAI.DirectionalTransience.markedArrayLaw line 66
  11. lemma OAI.DirectionalTransience.markedArrayLaw_probability line 69
  12. lemma OAI.DirectionalTransience.markedArrayLaw_fst line 76
  13. lemma OAI.DirectionalTransience.markedArrayLaw_ae line 80
  14. lemma OAI.DirectionalTransience.markedArrayLaw_supported line 91
  15. lemma OAI.DirectionalTransience.StationaryArrayLaw.marked_preserving line 105