DiskCrossing.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Planar disk crossing by covering-angle lifting.

lemma OAI.PlanarL1.Topology.rectangle_zero line 14

Source documentation

The planar rectangle crossing obstruction, proved by lifting angles rather than assuming a Jordan separation theorem.

lemma rectangle_zero (F : C(unitInterval × unitInterval, ℂ))
    (hleft : ∀ t, (F (0,t)).re < 0)
    (hright : ∀ t, 0 < (F (1,t)).re)
    (hbottom : ∀ s, 0 < (F (s,0)).im)
    (htop : ∀ s, (F (s,1)).im < 0) :
    ∃ p, F p=0 := by
…

lemma OAI.PlanarL1.Topology.disk_re_lt_one line 90
lemma OAI.PlanarL1.Topology.disk_im_lt_one line 99

lemma OAI.PlanarL1.Topology.disk_opposite_arcs_meet line 110

Source documentation

Opposite endpoints in a disk force two continuous arcs to meet. This is one normal form of nonalternation.

lemma disk_opposite_arcs_meet (f g : C(unitInterval, ℂ))
    (hf : ∀ s, ‖f s‖ ≤ 1) (hg : ∀ t, ‖g t‖ ≤ 1)
    (hf0 : f 0 = -1) (hf1 : f 1 = 1)
    (hg0 : g 0 = -Complex.I) (hg1 : g 1 = Complex.I) :
    ∃ s t, f s=g t := by
…

def OAI.PlanarL1.Topology.annularConnector line 170
Source comment
An explicit annular extension reduces arbitrary cyclic boundary endpoints to the already-proved cardinal-endpoint disk crossing obstruction.
```
noncomputable def annularConnector (a b : ℝ) :
    Path (Circle.exp a : ℂ) ((2 : ℂ) * (Circle.exp b : ℂ)) where
…
```
lemma OAI.PlanarL1.Topology.norm_annularConnector line 178
lemma OAI.PlanarL1.Topology.annularConnector_disjoint line 185
lemma OAI.PlanarL1.Topology.annularConnector_disk line 227
Source documentation
An annular connector meets the closed unit disk only at its source.
```
lemma annularConnector_disk {a b : ℝ} {z : ℂ}
    (hz : z ∈ range (annularConnector a b)) (hn : ‖z‖ ≤ 1) :
    z = (Circle.exp a : ℂ) := by
…
```
Mentions: OAI.PlanarL1.Topology.annularConnector
lemma OAI.PlanarL1.Topology.annularConnector_disjoint_disk line 236
lemma OAI.PlanarL1.Topology.annular_extension_bound line 243

lemma OAI.PlanarL1.Topology.disk_cyclic_arcs_meet line 265

Source documentation

Arbitrary four boundary endpoints in strict cyclic order, with no injectivity requirement on either of the two disk paths.

lemma disk_cyclic_arcs_meet (a₀ a₁ a₂ a₃ : ℝ)
    (h₀₁ : a₀ < a₁) (h₁₂ : a₁ < a₂) (h₂₃ : a₂ < a₃)
    (hspan : a₃ < a₀ + 2 * π)
    (f : Path (Circle.exp a₀ : ℂ) (Circle.exp a₂ : ℂ))
    (g : Path (Circle.exp a₁ : ℂ) (Circle.exp a₃ : ℂ))
    (hf : ∀ s, ‖f s‖ ≤ 1) (hg : ∀ s, ‖g s‖ ≤ 1) :
    ∃ s t, f s = g t := by
…

lemma OAI.PlanarL1.Topology.noncrossing_of_disk_arcs line 348

Source documentation

Disjoint disk arcs with cyclically ordered boundary positions give exactly the combinatorial noncrossing relation used by column models. This is the final step of the complementary-disk argument.

lemma noncrossing_of_disk_arcs {n : ℕ} (G : SimpleGraph (Fin n))
    (angle : Fin n → ℝ) (horder : StrictMono angle)
    (hspan : ∀ i j, angle j - angle i < 2 * π)
    (arc : ∀ i j, G.Adj i j → Path (Circle.exp (angle i) : ℂ)
      (Circle.exp (angle j) : ℂ))
    (hdisk : ∀ i j h t, ‖arc i j h t‖ ≤ 1)
    (hdisjoint : ∀ i j h k l h', i ≠ k → i ≠ l → j ≠ k → j ≠ l →
      Disjoint (range (arc i j h)) (range (arc k l h'))) :
    PlanarL1.ColumnOrder.Noncrossing G := by
…

Mentions: OAI.PlanarL1.ColumnOrder.Noncrossing