OAI/Probability/SLE/Loewner/VerticalMapDerivative.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The derivative of a holomorphic inverse limit is determined by its explicit values on the positive imaginary axis.
- lemma
OAI.SLEExactGauge.vertical_axis_derivativeline 13