SerpentineUpperHalfPlane.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The complete normal ribbon starts on the real boundary and every positive longitudinal coordinate lies in the upper half-plane.

lemma OAI.SLEExactGauge.Serpentine.lowConnector_normal_im_pos line 13
theorem OAI.SLEExactGauge.Serpentine.complete_normal_upper line 67
Source documentation
The actual entire ribbon lies above the real boundary at every positive longitudinal parameter.
```
theorem complete_normal_upper {m : ℕ} (hm : 0 < m) {H r X Y : ℝ}
    (hH : 1 < H) (hr : 1 < r) (hX : 2 * r < X) (hY : 300 * (m : ℝ) < Y)
    {z : ℂ} (hz : 0 < z.re) (ha : |z.im| ≤ 1) :
    0 < (normalRibbon (completeSpine m H r X Y) (completeTangent m H r X Y) z).im := by
…
```
Mentions: OAI.SLEExactGauge.Serpentine.normalRibbon, OAI.SLEExactGauge.Serpentine.completeSpine, OAI.SLEExactGauge.Serpentine.completeTangent