OAI/Probability/SLE/Geometry/TransverseCurveDifference.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A transverse crossing of two smooth planar curves is a locally injective zero of their two-parameter difference map.

  1. lemma OAI.SLEExactGauge.exists_injective_closedBall_of_strict_deriv line 14
  2. lemma OAI.SLEExactGauge.transverse_difference_locally_injective line 27
  3. lemma OAI.SLEExactGauge.transverse_radial_angular line 56