OAI/Probability/SLE/Gauge/SerpentineTerminal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SLEExactGauge.Serpentine.turnPoint_column_ne_nonadjacent line 12

   Source documentation

   A turn cannot meet any column except its two attached columns, regardless of the height on that column.

   theorem turnPoint_column_ne_nonadjacent {h : ℝ} (hh : 0 < h) {m i k : ℕ} (hm : 0 < m)
       (hk : k < i ∨ i + 2 ≤ k) (c : ℂ) (t y : ℝ) {a b : ℝ}
       (ha : |a| ≤ 1) (hb : |b| ≤ 1) :
       turnPoint c h m i t a ≠ columnPoint c h m k y b := by
   …

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

2. lemma OAI.SLEExactGauge.Serpentine.side_even line 34
3. theorem OAI.SLEExactGauge.Serpentine.turnPoint_terminal_column_ne line 40

   Source documentation

   The upward terminal continuation is disjoint from every turn. The preceding turn bends downwards; earlier turns are horizontally separated from the terminal column.

   theorem turnPoint_terminal_column_ne {h : ℝ} (hh : 0 < h) {m i : ℕ} (hm : 0 < m)
       (hi : i < 2 * m) (c : ℂ) {t y a b : ℝ} (ht : t ∈ Icc 0 Real.pi)
       (hy : h < y) (ha : |a| ≤ 1) (hb : |b| ≤ 1) :
       turnPoint c h m i t a ≠ columnPoint c h m (2 * m) y b := by
   …

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