OAI/Probability/SLE/Gauge/ActualDenseGoodState.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The dense experiment at an actual finite stopping time, conditional on its live good-angle radius state. Constants are chosen before the stopping time, marked point and stopped-past event.

  1. lemma OAI.SLEExactGauge.measurable_actual_radius_level line 25
  2. lemma OAI.SLEExactGauge.measurable_actual_stopped_mass_test line 40
  3. theorem OAI.SLEExactGauge.uniform_actual_dense_at_good_radius_state line 55