OAI/Probability/SLE/Geometry/ConditionalStopExtension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A conditional estimate at finite stopping times extends unchanged to a stopping time finite almost surely on its admissible stopped-past event. The geometric state is evaluated only on that event.

  1. theorem OAI.SLEExactGauge.conditional_event_bound_at_extended_stop line 15