OAI/Probability/SLE/Geometry/ExtendedStopLocalization.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Finite localization of a possibly infinite stopping time. The value S.untopD 0 is used only on the event where S is finite; it is not asserted to be a stopping time on the whole sample space.

  1. def OAI.SLEExactGauge.finiteStopEvent line 17
  2. lemma OAI.SLEExactGauge.cutoffStop_le_horizon line 20

    Distinct definitions of this name: OAI/Probability/SLE/Multipoint/MultipointRadiusSwitches.lean:54 (different declaration text). Qualify references as OAI.SLEExactGauge.cutoffStop_le_horizon@path.

  3. lemma OAI.SLEExactGauge.cutoffStop_le_stop line 24
  4. lemma OAI.SLEExactGauge.cutoffStop_monotone line 29
  5. lemma OAI.SLEExactGauge.finiteStopEvent_mono line 36
  6. lemma OAI.SLEExactGauge.iUnion_finiteStopEvent line 42
  7. lemma OAI.SLEExactGauge.cutoffStop_eqOn_finiteStopEvent line 55
  8. lemma OAI.SLEExactGauge.cutoffStop_eventually_eq line 60
  9. lemma OAI.SLEExactGauge.finiteStopEvent_measurable line 74
  10. lemma OAI.SLEExactGauge.finiteStopEvent_measurable_cutoff line 78
  11. lemma OAI.SLEExactGauge.finiteStopEvent_inter_measurable_cutoff line 83
  12. lemma OAI.SLEExactGauge.finiteStopEvent_all_measurable line 88
  13. lemma OAI.SLEExactGauge.cutoffStop_past_le line 93
  14. lemma OAI.SLEExactGauge.ae_of_cutoffStop line 97
  15. lemma OAI.SLEExactGauge.sourceRestartDriverPath_eq_on_finiteStopEvent line 109