OAI/Probability/SLE/Multipoint/MultipointPhaseProcess.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual finite phase process read from the three stopping times of each marked point.

  1. def OAI.SLEExactGauge.Multipoint.phaseAt line 15
  2. def OAI.SLEExactGauge.Multipoint.phaseOfPattern line 20
  3. lemma OAI.SLEExactGauge.Multipoint.phaseAt_of_pattern line 23
  4. lemma OAI.SLEExactGauge.Multipoint.phaseAt_monotone line 31
  5. lemma OAI.SLEExactGauge.Multipoint.phaseAt_ge_iff line 40
  6. lemma OAI.SLEExactGauge.Multipoint.phaseAt_const_sorted_interval line 48
  7. lemma OAI.SLEExactGauge.Multipoint.phaseAt_crossed_sorted_switch line 59
  8. lemma OAI.SLEExactGauge.Multipoint.phaseAt_horizon line 74