OAI/Probability/Ballisticity/Estimates/SelectedBoundaryRestart.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.selectedBoundaryAt line 15
  2. def OAI.DirectionalTransience.selectedAdmissibleBoundaryPrefix line 22
  3. lemma OAI.DirectionalTransience.selectedBoundaryPrefix_characterization line 36
  4. lemma OAI.DirectionalTransience.selectedBoundaryAt_unique line 93
  5. lemma OAI.DirectionalTransience.selectedBoundaryAt_exists line 112
  6. lemma OAI.DirectionalTransience.selectedMeasurableSet_boundaryAt line 119
  7. lemma OAI.DirectionalTransience.selectedBoundaryCode_exists line 135
  8. def OAI.DirectionalTransience.selectedBoundaryCode line 143
  9. def OAI.DirectionalTransience.selectedBoundaryTimes line 146
  10. lemma OAI.DirectionalTransience.measurable_selectedBoundaryCode line 149
  11. lemma OAI.DirectionalTransience.measurable_selectedBoundaryTimes line 159
  12. lemma OAI.DirectionalTransience.selectedBoundaryTimes_spec line 162
  13. lemma OAI.DirectionalTransience.selectedBoundaryTimes_eq line 167
  14. def OAI.DirectionalTransience.selectedBoundaryAtom line 172
  15. lemma OAI.DirectionalTransience.selectedMeasurableSet_selectedBoundaryAtom line 177
  16. lemma OAI.DirectionalTransience.selectedBoundaryAtom_eq line 183
  17. lemma OAI.DirectionalTransience.shared_selectedBoundaryAtom_map line 201
  18. def OAI.DirectionalTransience.selectedBoundaryData line 216
  19. lemma OAI.DirectionalTransience.selectedBoundaryData_fiber line 220
  20. lemma OAI.DirectionalTransience.measurable_selectedBoundaryData line 243
  21. def OAI.DirectionalTransience.selectedBoundarySuffix line 251
  22. lemma OAI.DirectionalTransience.measurable_selectedBoundarySuffix line 254
  23. lemma OAI.DirectionalTransience.selectedBoundaryData_times line 261
  24. lemma OAI.DirectionalTransience.selectedBoundaryAtom_fiber_ae line 265
  25. lemma OAI.DirectionalTransience.selectedBoundaryAt_exists_above line 284
  26. lemma OAI.DirectionalTransience.shared_selectedBoundaryTimes_spec line 292
  27. def OAI.DirectionalTransience.BoundaryData.endpoints line 311
  28. lemma OAI.DirectionalTransience.shared_selectedBoundaryData_map line 314
  29. lemma OAI.DirectionalTransience.lintegral_countable_restart_dependent line 339
  30. theorem OAI.DirectionalTransience.shared_selected_jointPast_restart line 365