OAI/Probability/SLE/Geometry/NormalizedRestartGoodSet.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every measurable full-law certificate is retained by the randomly normalized fresh driver, on the original probability space.

  1. lemma OAI.SLEExactGauge.normalized_restart_mem_full_driver_set line 15