OAI/Probability/SLE/Gauge/SerpentineCompleteCurve.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Arclength gluing of the low rounded connector and the upward-continued serpentine array.

  1. lemma OAI.SLEExactGauge.Serpentine.arraySpine_zero line 15
  2. lemma OAI.SLEExactGauge.Serpentine.arrayTangent_zero line 25
  3. lemma OAI.SLEExactGauge.Serpentine.lowConnector_after line 33
  4. def OAI.SLEExactGauge.Serpentine.connectorEntry line 39
  5. def OAI.SLEExactGauge.Serpentine.arrayCenter line 41
  6. def OAI.SLEExactGauge.Serpentine.completeSpine line 44
  7. def OAI.SLEExactGauge.Serpentine.completeTangent line 48
  8. lemma OAI.SLEExactGauge.Serpentine.completeSpine_hasDerivAt line 52
  9. lemma OAI.SLEExactGauge.Serpentine.completeTangent_norm line 71
  10. lemma OAI.SLEExactGauge.Serpentine.completeTangent_lipschitz line 77
  11. lemma OAI.SLEExactGauge.Serpentine.complete_normal_patch_bounds line 88