OAI/Probability/SLE/Gauge/VaryingPassageEvents.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The rc:varying-good-events step of the ribbon argument. Positivity of a conditional passage probability on one event gives a fixed lower probability after intersecting with varying early-containment events. No uniform conditional passage bound is assumed.

  1. theorem OAI.SLEExactGauge.varying_passage_events_lower_bound line 18