OAI/Probability/SLE/Gauge/SerpentineEmbedding.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The only contacts between the straight and circular normal bands are their prescribed common end sections. These geometric statements support the global embedding of the concatenated serpentine.

  1. lemma OAI.SLEExactGauge.Serpentine.turnPoint_im line 14
  2. lemma OAI.SLEExactGauge.Serpentine.turnPoint_oriented_im line 21
  3. lemma OAI.SLEExactGauge.Serpentine.columnPoint_equal_forces_index line 31
  4. lemma OAI.SLEExactGauge.Serpentine.columnPoint_injective line 39
  5. theorem OAI.SLEExactGauge.Serpentine.turnPoint_column_contact line 57

    Source documentation

    A circular normal band can meet a straight band only at angle zero or pi; its interior lies strictly above or below all straight passes.

    theorem turnPoint_column_contact {h : ℝ} (hh : 0 < h) {m j k : ℕ} (hm : 0 < m)
    (c : ℂ) {t y a b : ℝ} (ht : t ∈ Icc 0 Real.pi) (hy : |y| ≤ h)
    (ha : |a| ≤ 1) (he : turnPoint c h m j t a = columnPoint c h m k y b) :
    t = 0 ∨ t = Real.pi := by
…

    Mentions: OAI.SLEExactGauge.Serpentine.turnPoint, OAI.SLEExactGauge.Serpentine.columnPoint

  6. theorem OAI.SLEExactGauge.Serpentine.turnPoint_column_gluing line 78

    Source documentation

    Exact gluing sections, including the matching normal coordinate.

    theorem turnPoint_column_gluing {h : ℝ} (hh : 0 < h) {m j k : ℕ} (hm : 0 < m)
    (c : ℂ) {t y a b : ℝ} (ht : t ∈ Icc 0 Real.pi) (hy : |y| ≤ h)
    (ha : |a| ≤ 1) (hb : |b| ≤ 1)
    (he : turnPoint c h m j t a = columnPoint c h m k y b) :
    (t = 0 ∧ k = j ∧ y = side j * h ∧ a = b) ∨
      (t = Real.pi ∧ k = j + 1 ∧ y = side j * h ∧ a = b) := by
…

    Mentions: OAI.SLEExactGauge.Serpentine.turnPoint, OAI.SLEExactGauge.Serpentine.columnPoint, OAI.SLEExactGauge.Serpentine.side

  7. lemma OAI.SLEExactGauge.Serpentine.turnPoint_re line 96
  8. lemma OAI.SLEExactGauge.Serpentine.turn_horizontal_bound line 104
  9. lemma OAI.SLEExactGauge.Serpentine.turn_oriented_height line 123
  10. theorem OAI.SLEExactGauge.Serpentine.turnPoint_ne line 132

    Source documentation

    Different circular turns have disjoint full normal bands. Neighboring turns lie on opposite sides; all other turn pairs have horizontal clearance.

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

    Mentions: OAI.SLEExactGauge.Serpentine.turnPoint