OAI/Combinatorics/BalancedRyser/Probability/FiniteHistory.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.FiniteHistory.Prefix line 15
  2. abbrev OAI.Balanced.FiniteHistory.Path line 16
  3. def OAI.Balanced.FiniteHistory.historyKernel line 18
  4. instance OAI.Balanced.FiniteHistory.historyKernel_isMarkov line 21
  5. def OAI.Balanced.FiniteHistory.pathLaw line 27
  6. instance OAI.Balanced.FiniteHistory.pathLaw_isProbability line 30
  7. def OAI.Balanced.FiniteHistory.filtration line 35
  8. def OAI.Balanced.FiniteHistory.stepObservable line 38
  9. lemma OAI.Balanced.FiniteHistory.measurable_stepObservable line 41
  10. lemma OAI.Balanced.FiniteHistory.integrable_stepObservable line 47
  11. lemma OAI.Balanced.FiniteHistory.map_next_traj line 55
  12. lemma OAI.Balanced.FiniteHistory.integral_stepObservable_traj line 61
  13. theorem OAI.Balanced.FiniteHistory.condExp_stepObservable line 78
  14. theorem OAI.Balanced.FiniteHistory.map_prefix_pathLaw line 89
  15. theorem OAI.Balanced.FiniteHistory.map_prefix_next_pathLaw line 94