OAI/Probability/SLE/Mass/RestartRandomMassTesting.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The fresh-driver law may be tested against a random spatial weight measurable in the stopped past. This is the conditional-Tonelli step for the restart candidate, before invoking uniqueness.

  1. lemma OAI.SLEExactGauge.fresh_mass_test_joint_measurable line 16
  2. theorem OAI.SLEExactGauge.restart_random_mass_test line 27