OAI/Probability/Ballisticity/Estimates/CommonBoundaryRestart.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.truePairCylinder line 16
  2. lemma OAI.DirectionalTransience.measurableSet_truePairCylinder line 20
  3. lemma OAI.DirectionalTransience.truePairCylinder_future line 25
  4. lemma OAI.DirectionalTransience.truePairCylinder_noDrop line 51
  5. lemma OAI.DirectionalTransience.shared_truePairCylinder_map line 67
  6. def OAI.DirectionalTransience.BoundaryAt line 108
  7. def OAI.DirectionalTransience.AdmissibleBoundaryPrefix line 115
  8. lemma OAI.DirectionalTransience.boundaryPrefix_characterization line 129
  9. lemma OAI.DirectionalTransience.boundaryAt_unique line 186
  10. lemma OAI.DirectionalTransience.boundaryAt_exists line 205
  11. lemma OAI.DirectionalTransience.measurableSet_boundaryAt line 212
  12. lemma OAI.DirectionalTransience.boundaryCode_exists line 229
  13. def OAI.DirectionalTransience.boundaryCode line 237
  14. def OAI.DirectionalTransience.boundaryTimes line 240
  15. lemma OAI.DirectionalTransience.measurable_boundaryCode line 243
  16. lemma OAI.DirectionalTransience.measurable_boundaryTimes line 253
  17. lemma OAI.DirectionalTransience.boundaryTimes_spec line 256
  18. lemma OAI.DirectionalTransience.boundaryTimes_eq line 261
  19. def OAI.DirectionalTransience.boundaryAtom line 266
  20. lemma OAI.DirectionalTransience.measurableSet_boundaryAtom line 271
  21. lemma OAI.DirectionalTransience.boundaryAtom_eq line 277
  22. lemma OAI.DirectionalTransience.shared_boundaryAtom_map line 295
  23. lemma OAI.DirectionalTransience.boundary_exists_of_commonLayer line 310
  24. lemma OAI.DirectionalTransience.shared_boundaryTimes_spec line 336