OAI/Analysis/LipschitzHilbert/Estimates/FirstExceed.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Disjoint first-crossing events for a finite scalar process.

  1. def OAI.LipschitzHilbert.firstExceed line 17
  2. def OAI.LipschitzHilbert.finiteMaxEvent line 20
  3. theorem OAI.LipschitzHilbert.firstExceed_disjoint line 23
  4. theorem OAI.LipschitzHilbert.firstExceed_union line 32
  5. theorem OAI.LipschitzHilbert.measurableSet_firstExceed line 49
  6. theorem OAI.LipschitzHilbert.firstExceed_measure_sum line 58
  7. theorem OAI.LipschitzHilbert.firstExceed_norm_overshoot line 73
  8. theorem OAI.LipschitzHilbert.firstExceed_large_subset line 89