OAI/Probability/SLE/Mass/CanonicalMassFirstVisit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

At each fixed time the canonical mass is the terminal measure restricted to the already visited trace.

  1. lemma OAI.SLEExactGauge.Multipoint.halfPlaneStoppingGreenMeasure_const line 16
  2. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.atTime_eq_restrict_past line 25