OAI/Probability/SLE/Geometry/CurveJoin.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Joining the straight and circular pieces of the serpentine at matching positions and tangents. The joins preserve the actual derivative and the common tangent Lipschitz constant.

  1. def OAI.SLEExactGauge.Serpentine.curveJoin line 15
  2. lemma OAI.SLEExactGauge.Serpentine.curveJoin_of_le line 17
  3. lemma OAI.SLEExactGauge.Serpentine.curveJoin_of_gt line 20
  4. theorem OAI.SLEExactGauge.Serpentine.curveJoin_continuous line 23
  5. lemma OAI.SLEExactGauge.Serpentine.curveJoin_lipschitz line 32
  6. theorem OAI.SLEExactGauge.Serpentine.curveJoin_hasDerivAt line 65