OAI/Probability/SLE/Geometry/RoundedConnectorBands.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Embedded normal bands over the quarter-circles of the connector.

  1. def OAI.SLEExactGauge.Serpentine.quarterNormal line 12
  2. def OAI.SLEExactGauge.Serpentine.upperQuarterNormal line 15
  3. lemma OAI.SLEExactGauge.Serpentine.quarterNormal_eq line 18
  4. lemma OAI.SLEExactGauge.Serpentine.quarter_angle_bound line 25
  5. lemma OAI.SLEExactGauge.Serpentine.quarterNormal_bounds line 33
  6. lemma OAI.SLEExactGauge.Serpentine.upperQuarterNormal_reverse line 54
  7. lemma OAI.SLEExactGauge.Serpentine.upperQuarterNormal_bounds line 61