OAI/Analysis/MarkovType/FiniteStoppingTime.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MarkovSuperreflexivity.FinitePartitionFiltration line 9
  2. def OAI.MarkovSuperreflexivity.FinitePartitionFiltration.IsStoppingTime line 18
  3. def OAI.MarkovSuperreflexivity.FinitePartitionFiltration.IsPredictableTime line 21
  4. def OAI.MarkovSuperreflexivity.FinitePartitionFiltration.AdaptedAt line 25
  5. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.adaptedAt_mono line 28
  6. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.isStoppingTime_const line 33
  7. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.isStoppingTime_of_isPredictableTime line 37
  8. def OAI.MarkovSuperreflexivity.FinitePartitionFiltration.stoppedSetoid line 53
  9. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.stopped_rel_of_rel_of_le line 70
  10. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.stoppedSetoid_refines line 80
  11. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.adapted_stopped line 86
  12. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.stopped_atom_and_predictable_eq line 93