OAI/Probability/SLE/Geometry/RoundedConnector.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

The two quarter-circles used by the low connector from the real boundary to the first serpentine column. The radius is measured in ribbon-width units, so a radius at least fifty gives the same derivative and tangent bounds as the array.

  1. def OAI.SLEExactGauge.Serpentine.quarterLength line 16
  2. def OAI.SLEExactGauge.Serpentine.quarterBend line 18
  3. def OAI.SLEExactGauge.Serpentine.quarterTangent line 21
  4. def OAI.SLEExactGauge.Serpentine.upperQuarter line 23
  5. def OAI.SLEExactGauge.Serpentine.upperQuarterTangent line 26
  6. lemma OAI.SLEExactGauge.Serpentine.quarterBend_eq line 28
  7. lemma OAI.SLEExactGauge.Serpentine.quarterTangent_eq line 38
  8. lemma OAI.SLEExactGauge.Serpentine.quarterBend_hasDerivAt line 45
  9. lemma OAI.SLEExactGauge.Serpentine.quarterTangent_norm line 60
  10. lemma OAI.SLEExactGauge.Serpentine.quarterTangent_lipschitz line 63
  11. lemma OAI.SLEExactGauge.Serpentine.quarterBend_zero line 82
  12. lemma OAI.SLEExactGauge.Serpentine.quarterTangent_zero line 85
  13. lemma OAI.SLEExactGauge.Serpentine.quarterBend_end line 88
  14. lemma OAI.SLEExactGauge.Serpentine.quarterTangent_end line 93
  15. lemma OAI.SLEExactGauge.Serpentine.upperQuarter_hasDerivAt line 98
  16. lemma OAI.SLEExactGauge.Serpentine.upperQuarterTangent_norm line 107
  17. lemma OAI.SLEExactGauge.Serpentine.upperQuarterTangent_lipschitz line 110
  18. lemma OAI.SLEExactGauge.Serpentine.upperQuarter_zero line 117
  19. lemma OAI.SLEExactGauge.Serpentine.upperQuarter_end line 120
  20. lemma OAI.SLEExactGauge.Serpentine.upperQuarterTangent_zero line 124
  21. lemma OAI.SLEExactGauge.Serpentine.upperQuarterTangent_end line 127