OAI/Analysis/CircleDomains/Probability/ExitTimeMeasurability.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Borel first-exit and last-entry locations for the collar crossing laws.

  1. theorem OAI.CircleDomainRigidity.firstExit_notMem_of_exists line 16
  2. theorem OAI.CircleDomainRigidity.lt_firstExit_iff_mapsTo line 20
  3. theorem OAI.CircleDomainRigidity.measurable_firstExitTime line 37
  4. theorem OAI.CircleDomainRigidity.continuous_reversedPath line 52
  5. theorem OAI.CircleDomainRigidity.measurable_lastEntryTime line 55
  6. theorem OAI.CircleDomainRigidity.measurable_lastEntryLocation line 60
  7. theorem OAI.CircleDomainRigidity.mem_after_lastEntry line 66