SerpentineCompleteEmbedding.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The low connector and the complete infinite array have one common normal cross-section. Hence the entire prescribed ribbon is embedded.

lemma OAI.SLEExactGauge.Serpentine.complete_normal_of_le line 15
lemma OAI.SLEExactGauge.Serpentine.complete_normal_of_gt line 21
lemma OAI.SLEExactGauge.Serpentine.complete_normal_cross_disjoint line 30
theorem OAI.SLEExactGauge.Serpentine.complete_normal_injective line 81
Source documentation
Global embedding of the whole explicit normal ribbon, including its real-boundary connector and infinite final vertical continuation.
```
theorem complete_normal_injective {m : ℕ} (hm : 0 < m) {H r X Y : ℝ}
    (hr : 50 ≤ r) (hX : 2 * r < X) (hY : H + 2 * r + 1 + 300 * m < Y) :
    InjOn (normalRibbon (completeSpine m H r X Y) (completeTangent m H r X Y))
      {z : ℂ | 0 ≤ z.re ∧ |z.im| ≤ 1} := by
…
```
Mentions: OAI.SLEExactGauge.Serpentine.normalRibbon, OAI.SLEExactGauge.Serpentine.completeSpine, OAI.SLEExactGauge.Serpentine.completeTangent