OAI/Probability/SLE/Geometry/EndpointMonotonicity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One-sided derivative comparisons remain valid at a continuous endpoint, even when the derivative at that endpoint is singular.

  1. lemma OAI.SLEExactGauge.le_initial_of_deriv_nonpos_on_Ioc line 13