OAI/Probability/SLE/Loewner/StoppedInverseTerminalUniqueness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite-time restart identity extends to the locally exhausted terminal mass using the same raw fresh functional.

  1. lemma OAI.SLEExactGauge.Multipoint.halfPlane_nested_remainder line 18
  2. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.stoppedFreshTerminalMass_eq_remainder line 50