OAI/Probability/SLE/Gauge/SerpentinePieces.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Unit-speed straight and semicircular pieces in ribbon-width units. Their tangents match at each join and have the uniform Lipschitz bound 1/50 required by the fixed local ribbon constants.

  1. def OAI.SLEExactGauge.Serpentine.straightPiece line 16
  2. def OAI.SLEExactGauge.Serpentine.straightTangent line 20
  3. def OAI.SLEExactGauge.Serpentine.circularPiece line 22
  4. def OAI.SLEExactGauge.Serpentine.circularTangent line 26
  5. lemma OAI.SLEExactGauge.Serpentine.straightPiece_hasDerivAt line 29
  6. lemma OAI.SLEExactGauge.Serpentine.circularPiece_hasDerivAt line 35
  7. lemma OAI.SLEExactGauge.Serpentine.straightTangent_norm line 46
  8. lemma OAI.SLEExactGauge.Serpentine.circularTangent_norm line 50
  9. lemma OAI.SLEExactGauge.Serpentine.circularTangent_hasDerivAt line 60
  10. lemma OAI.SLEExactGauge.Serpentine.circularTangent_deriv_norm line 70
  11. lemma OAI.SLEExactGauge.Serpentine.circularTangent_lipschitz line 84
  12. lemma OAI.SLEExactGauge.Serpentine.straight_circular_position_match line 90
  13. lemma OAI.SLEExactGauge.Serpentine.circular_straight_position_match line 99
  14. lemma OAI.SLEExactGauge.Serpentine.straight_circular_tangent_match line 106
  15. lemma OAI.SLEExactGauge.Serpentine.circular_straight_tangent_match line 109