OAI/Probability/SLE/Geometry/OpenBoundaryTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The terminal value of a reverse path does not require a derivative beyond its interval of definition. A linear continuation supplies the unused terminal right derivative without changing the path.

  1. theorem OAI.SLEExactGauge.Target.boundary_reverse_eq_trace_of_open_derivative line 14