OAI/Probability/SLE/Loewner/RawRestartCanonical.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One fixed raw canonical mass works at every finite Brownian restart. The finite process is progressive in the shifted past and locally exhausts its own terminal measure on one full event for each restart.

  1. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.exists_raw_restarted_canonical line 19