OAI/Probability/SLE/Angle/TargetPotentialMeasurability.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The exact prescribed disk potential is a measurable path functional. All definitions, including the killed flow and its time integral, are retained on every continuous based driver.

  1. lemma OAI.SLEExactGauge.Target.measurable_diskMapInv line 15
  2. lemma OAI.SLEExactGauge.Target.measurable_initialRadius line 19
  3. lemma OAI.SLEExactGauge.Target.measurable_clockIntegrand line 23
  4. lemma OAI.SLEExactGauge.Target.measurable_clock line 44
  5. lemma OAI.SLEExactGauge.Target.measurable_angle line 68
  6. lemma OAI.SLEExactGauge.Target.measurable_radius line 85
  7. lemma OAI.SLEExactGauge.Target.measurableSet_disk_surviving line 90
  8. lemma OAI.SLEExactGauge.Target.measurable_green line 99
  9. lemma OAI.SLEExactGauge.Target.measurable_potential line 108
  10. lemma OAI.SLEExactGauge.Target.clock_stopDriver line 114
  11. lemma OAI.SLEExactGauge.Target.green_stopDriver line 131
  12. lemma OAI.SLEExactGauge.Target.potential_stopDriver line 138
  13. lemma OAI.SLEExactGauge.Target.potential_measurable_past line 145
  14. theorem OAI.SLEExactGauge.Target.potential_continuation_condLExp line 150
  15. theorem OAI.SLEExactGauge.Target.potential_continuation_finite_condExp line 157