OAI/Probability/SLE/Geometry/HarmonicExitProbability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Positive bounded harmonic terminal tests control finite-exit events without requiring measurability of the event's existential description.

  1. lemma OAI.SLEExactGauge.terminal_threshold_measure_le line 14
  2. theorem OAI.SLEExactGauge.SmoothDomainExhaustion.nonnegative_harmonic_exit_bound line 29