OAI/Probability/SLE/Gauge/SerpentineTerminalGuide.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The actual last front is on the terminal vertical piece. Its access guide reaches height two before the explicit marked hook is attached.

  1. def OAI.SLEExactGauge.Serpentine.fitEntry line 14
  2. def OAI.SLEExactGauge.Serpentine.fitCompletion line 17
  3. def OAI.SLEExactGauge.Serpentine.fitTerminalX line 19
  4. def OAI.SLEExactGauge.Serpentine.fitTerminalHeight line 21
  5. def OAI.SLEExactGauge.Serpentine.fitHighTime line 25
  6. lemma OAI.SLEExactGauge.Serpentine.fitCompletion_bounds line 28
  7. lemma OAI.SLEExactGauge.Serpentine.fit_scaledY line 45
  8. lemma OAI.SLEExactGauge.Serpentine.fitTerminalHeight_bounds line 50
  9. lemma OAI.SLEExactGauge.Serpentine.physicalFitChart_terminal line 63
  10. lemma OAI.SLEExactGauge.Serpentine.fitHighTime_large line 89
  11. lemma OAI.SLEExactGauge.Serpentine.physicalFitChart_terminal_guide line 99

    Source documentation

    Exact physical formula for the tapered terminal access guide.

    lemma physicalFitChart_terminal_guide {s : ℝ} (hs : 0 < s) (w : ℂ) (hw : s ≤ w.im)
    {m : ℕ} (hm : 0 < m) (x : ℝ) {t : ℝ} (ht : 0 ≤ t) :
    physicalFitChart s w m (guideCoordinate (fitCompletion s w m) x t) =
      ((fitTerminalX s w - ribbonWidth (halfHeight s) m * x * max (1 - 4 * t) 0 : ℝ) : ℂ) +
      ((fitTerminalHeight s w m + ribbonWidth (halfHeight s) m * t : ℝ) : ℂ) * Complex.I := by
…

    Mentions: OAI.SLEExactGauge.Serpentine.physicalFitChart, OAI.SLEExactGauge.Serpentine.fitCompletion, OAI.SLEExactGauge.Serpentine.fitTerminalX, OAI.SLEExactGauge.Serpentine.ribbonWidth, OAI.SLEExactGauge.Serpentine.halfHeight, OAI.SLEExactGauge.Serpentine.fitTerminalHeight

  12. lemma OAI.SLEExactGauge.Serpentine.physicalFitChart_terminal_guide_endpoint line 109
  13. lemma OAI.SLEExactGauge.Serpentine.physicalFitChart_terminal_guide_height line 123
  14. lemma OAI.SLEExactGauge.Serpentine.physicalFitChart_terminal_guide_strict_height line 135
  15. lemma OAI.SLEExactGauge.Serpentine.physicalFitChart_terminal_guide_injective line 147