OAI/Probability/SLE/Geometry/FirstSuccessfulPast.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The finite first-success partition in the strict past-mass identity. A later successful test outside the visited trace is detected by its first successful predecessor, whose entire event is already in that earlier past.

  1. def OAI.SLEExactGauge.Multipoint.firstPastSuccess line 18
  2. lemma OAI.SLEExactGauge.Multipoint.mem_firstPastSuccess_iff line 21
  3. lemma OAI.SLEExactGauge.Multipoint.exists_firstPastSuccess line 25
  4. lemma OAI.SLEExactGauge.Multipoint.firstPastSuccess_disjoint line 43
  5. lemma OAI.SLEExactGauge.Multipoint.firstPastSuccess_measurable line 53
  6. lemma OAI.SLEExactGauge.Multipoint.firstPastSuccess_future_union line 64
  7. lemma OAI.SLEExactGauge.Multipoint.firstPastSuccess_unique line 89
  8. lemma OAI.SLEExactGauge.Multipoint.firstPastSuccess_future_mass line 95