OAI/Probability/SLE/Loewner/SmoothDriverLipschitz.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A bounded derivative on nonnegative times gives a global Lipschitz bound for the driver's constant extension to negative times.

  1. theorem OAI.SLEExactGauge.Target.lipschitz_driverValue_of_bounded_derivative line 13