OAI/Probability/SLE/Loewner/TargetForwardAnalytic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Spatial analyticity of the raw forward map follows from the analytic inverse and its nonzero derivative.

  1. lemma OAI.SLEExactGauge.Target.differentiableOn_flow_of_inverse line 15