OAI/Probability/SLE/Geometry/RoundedConnectorCurve.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The actual arclength connector from zero to a distant vertical column: vertical, quarter-circle, horizontal, quarter-circle, then vertical.

  1. lemma OAI.SLEExactGauge.Serpentine.translate_curve_hasDerivAt line 14
  2. lemma OAI.SLEExactGauge.Serpentine.linear_curve_hasDerivAt line 22
  3. def OAI.SLEExactGauge.Serpentine.connectorSecond line 27
  4. def OAI.SLEExactGauge.Serpentine.connectorThird line 29
  5. def OAI.SLEExactGauge.Serpentine.connectorFourth line 31
  6. def OAI.SLEExactGauge.Serpentine.connectorInitial line 33
  7. def OAI.SLEExactGauge.Serpentine.connectorFirstTurn line 35
  8. def OAI.SLEExactGauge.Serpentine.connectorHorizontal line 38
  9. def OAI.SLEExactGauge.Serpentine.connectorLastTurn line 41
  10. def OAI.SLEExactGauge.Serpentine.connectorTail line 45
  11. def OAI.SLEExactGauge.Serpentine.lowConnector line 48
  12. def OAI.SLEExactGauge.Serpentine.lowConnectorTangent line 57
  13. lemma OAI.SLEExactGauge.Serpentine.connector_cuts line 66
  14. lemma OAI.SLEExactGauge.Serpentine.connector_position_matches line 75
  15. lemma OAI.SLEExactGauge.Serpentine.lowConnector_hasDerivAt line 96
  16. lemma OAI.SLEExactGauge.Serpentine.lowConnectorTangent_norm line 142