OAI/Probability/Ballisticity/Estimates/JointPastRestart.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.BoundaryData line 15
  2. instance OAI.DirectionalTransience.(instance at line 18) line 18
  3. instance OAI.DirectionalTransience.(instance at line 19) line 19
  4. instance OAI.DirectionalTransience.(instance at line 20) line 20
  5. def OAI.DirectionalTransience.boundaryData line 22
  6. lemma OAI.DirectionalTransience.boundaryData_fiber line 26
  7. lemma OAI.DirectionalTransience.measurable_boundaryData line 49
  8. def OAI.DirectionalTransience.boundarySuffix line 57
  9. lemma OAI.DirectionalTransience.measurable_boundarySuffix line 60
  10. lemma OAI.DirectionalTransience.boundaryData_times line 67
  11. lemma OAI.DirectionalTransience.boundaryAtom_fiber_ae line 71
  12. lemma OAI.DirectionalTransience.shared_boundaryData_map line 90
  13. lemma OAI.DirectionalTransience.lintegral_partition_countable line 118
  14. lemma OAI.DirectionalTransience.lintegral_countable_restart line 130
  15. theorem OAI.DirectionalTransience.shared_jointPast_restart line 159