OAI/Probability/SLE/Gauge/SerpentineLayout.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Explicit columns and circular turns for the dense-visit serpentine. The array and its normal bands fit in the displaced disk and stay a fixed distance from the marked point.

  1. def OAI.SLEExactGauge.Serpentine.side line 16
  2. lemma OAI.SLEExactGauge.Serpentine.side_abs line 18
  3. lemma OAI.SLEExactGauge.Serpentine.side_sq line 22
  4. def OAI.SLEExactGauge.Serpentine.displacementSign line 26
  5. def OAI.SLEExactGauge.Serpentine.center line 28
  6. def OAI.SLEExactGauge.Serpentine.halfHeight line 30
  7. def OAI.SLEExactGauge.Serpentine.spacing line 32
  8. def OAI.SLEExactGauge.Serpentine.turnRadius line 34
  9. def OAI.SLEExactGauge.Serpentine.ribbonWidth line 36
  10. def OAI.SLEExactGauge.Serpentine.columnOffset line 38
  11. def OAI.SLEExactGauge.Serpentine.columnPoint line 41

    Source documentation

    The closed width-one band over one straight pass, in physical scale.

    def columnPoint (c : ℂ) (h : ℝ) (m j : ℕ) (y a : ℝ) : ℂ :=
…
  12. def OAI.SLEExactGauge.Serpentine.turnPoint line 47

    Source documentation

    A circular connector, with its actual normal ribbon coordinate a. The parameter runs from zero to pi, alternating above and below.

    def turnPoint (c : ℂ) (h : ℝ) (m j : ℕ) (t a : ℝ) : ℂ :=
…
  13. lemma OAI.SLEExactGauge.Serpentine.center_dist line 53
  14. lemma OAI.SLEExactGauge.Serpentine.center_im line 59
  15. lemma OAI.SLEExactGauge.Serpentine.displaced_disk_inside line 62
  16. lemma OAI.SLEExactGauge.Serpentine.displaced_disk_separated line 71
  17. lemma OAI.SLEExactGauge.Serpentine.spacing_pos line 79
  18. lemma OAI.SLEExactGauge.Serpentine.turnRadius_pos line 82
  19. lemma OAI.SLEExactGauge.Serpentine.ribbonWidth_pos line 86
  20. lemma OAI.SLEExactGauge.Serpentine.spacing_eq_width line 90
  21. lemma OAI.SLEExactGauge.Serpentine.turnRadius_eq_width line 97
  22. lemma OAI.SLEExactGauge.Serpentine.columnOffset_bounds line 105
  23. lemma OAI.SLEExactGauge.Serpentine.width_le_halfHeight line 118
  24. lemma OAI.SLEExactGauge.Serpentine.radius_le_halfHeight line 125
  25. lemma OAI.SLEExactGauge.Serpentine.columnPoint_bound line 132
  26. lemma OAI.SLEExactGauge.Serpentine.turnPoint_zero line 154
  27. lemma OAI.SLEExactGauge.Serpentine.side_succ line 161
  28. lemma OAI.SLEExactGauge.Serpentine.turnPoint_pi line 164
  29. lemma OAI.SLEExactGauge.Serpentine.turn_direction_norm line 174
  30. lemma OAI.SLEExactGauge.Serpentine.turnPoint_bound line 185
  31. lemma OAI.SLEExactGauge.Serpentine.column_inside_displaced_disk line 225
  32. lemma OAI.SLEExactGauge.Serpentine.columnPoint_re line 236
  33. lemma OAI.SLEExactGauge.Serpentine.columnPoint_im line 241
  34. lemma OAI.SLEExactGauge.Serpentine.column_separation line 244
  35. lemma OAI.SLEExactGauge.Serpentine.columnPoint_ne line 269
  36. lemma OAI.SLEExactGauge.Serpentine.turn_radial_coefficient_pos line 279
  37. theorem OAI.SLEExactGauge.Serpentine.turnPoint_injective line 290

    Source documentation

    Each circular turn, with its full normal band, is embedded.

    theorem turnPoint_injective {h : ℝ} (hh : 0 < h) {m : ℕ} (hm : 0 < m)
    (c : ℂ) (j : ℕ) {t u a b : ℝ} (ht : t ∈ Icc 0 Real.pi)
    (hu : u ∈ Icc 0 Real.pi) (ha : |a| ≤ 1) (hb : |b| ≤ 1)
    (he : turnPoint c h m j t a = turnPoint c h m j u b) : t = u ∧ a = b := by
…

    Mentions: OAI.SLEExactGauge.Serpentine.turnPoint