OAI/Combinatorics/PlanarL1/TreeDisk.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarL1.Topology.exteriorToDisk line 16

   Source documentation

   Radial inversion fixes the unit circle and puts the exterior into the disk. This avoids any one-point-compactification assumption in the complementary region of a prospective tree neighborhood.

   noncomputable def exteriorToDisk (z : ℂ) : ℂ := star (z⁻¹)

2. lemma OAI.PlanarL1.Topology.exteriorToDisk_injective line 18
3. lemma OAI.PlanarL1.Topology.exteriorToDisk_circle line 22
4. lemma OAI.PlanarL1.Topology.exteriorToDisk_norm line 27
5. lemma OAI.PlanarL1.Topology.exteriorToDisk_continuous_path line 31
6. lemma OAI.PlanarL1.Topology.exterior_cyclic_arcs_meet line 42

   Source documentation

   The corresponding crossing theorem in the exterior of the unit disk. Inversion fixes every endpoint and is injective; no simplicity assumption on the two paths is needed.

   lemma exterior_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, 1 ≤ ‖f s‖) (hg : ∀ s, 1 ≤ ‖g s‖) :
       ∃ s t, f s = g t := by
   …

7. lemma OAI.PlanarL1.Topology.noncrossing_of_exterior_arcs line 62

   Source documentation

   Mutually disjoint exterior paths imply the literal noncrossing relation on the finite cyclic list of their boundary ports.

   lemma noncrossing_of_exterior_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) : ℂ))
       (hout : ∀ i j h t, 1 ≤ ‖arc i j h t‖)
       (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

8. lemma OAI.PlanarL1.Topology.circle_exp_arg line 80
9. lemma OAI.PlanarL1.Topology.finite_port_order line 87

   Source documentation

   A finite collection of distinct boundary ports supplies a cyclic list; angles in a single half-open turn handle the wrap-around without choosing a port as a special zero-angle endpoint.

   lemma finite_port_order {V : Type} [Fintype V] (port : V → ℂ)
       (hnorm : ∀ v, ‖port v‖ = 1) (hinj : Function.Injective port) :
       ∃ e : Fin (Fintype.card V) ≃ V,
         StrictMono (fun i => Complex.arg (port (e i))) ∧
         (∀ i j, Complex.arg (port (e j)) - Complex.arg (port (e i)) < 2 * π) := by
   …

10. lemma OAI.PlanarL1.Topology.convex_disk_coordinates line 108

    Source documentation

    Any bounded convex neighborhood has an ambient disk coordinate in which points outside its interior remain outside the open disk.

    lemma convex_disk_coordinates {S : Set ℂ} (hS : Convex ℝ S)
        (hne : (interior S).Nonempty) (hb : Bornology.IsBounded S) :
        ∃ h : ℂ ≃ₜ ℂ,
          (∀ z, z ∈ frontier S → ‖h z‖ = 1) ∧
          (∀ z, z ∉ interior S → 1 ≤ ‖h z‖) := by
    …

11. lemma OAI.PlanarL1.Topology.convex_ports_noncrossing line 129

    Source documentation

    Complementary arcs outside an actual convex tree-merging neighborhood produce a noncrossing cyclic order of its distinct leaf ports. All hypotheses here concern the geometric sets and paths, not a promised column model.

    lemma convex_ports_noncrossing {V : Type} [Fintype V] (G : SimpleGraph V)
        {S : Set ℂ} (hS : Convex ℝ S) (hne : (interior S).Nonempty)
        (hb : Bornology.IsBounded S) (port : V → ℂ)
        (hport : ∀ v, port v ∈ frontier S) (hinj : Function.Injective port)
        (arc : ∀ i j, G.Adj i j → Path (port i) (port j))
        (hout : ∀ i j h t, arc i j h t ∉ interior S)
        (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'))) :
        ∃ e : Fin (Fintype.card V) ≃ V,
          PlanarL1.ColumnOrder.Noncrossing (SimpleGraph.comap e G) := by
    …

    Mentions: OAI.PlanarL1.ColumnOrder.Noncrossing

12. lemma OAI.PlanarL1.Columns.interval_reachable line 169

    Source documentation

    An interval of selected consecutive indices is connected without using the wrap-around edge.

    lemma interval_reachable {n : ℕ} (G : SimpleGraph (Fin n)) (S : Set (Fin n))
        (he : ∀ i j, i.val+1=j.val → i∈S → j∈S → G.Adj i j)
        {i j : Fin n} (hij : i≤j) (hS : ∀ k, i≤k → k≤j → k∈S) :
        G.Reachable i j := by
    …

13. lemma OAI.PlanarL1.Columns.consecutive_connected line 194

    Source documentation

    The elementary circular-interval criterion: if a set and its complement have no alternating four indices, consecutive selected indices connect it.

    lemma consecutive_connected {n : ℕ} (G : SimpleGraph (Fin n)) (S : Set (Fin n))
        (he : ∀ i j, i≠j → Consecutive i j → i∈S → j∈S → G.Adj i j)
        (halt : ∀ a b c d : Fin n, a<b → b<c → c<d →
          ¬((a∈S ∧ b∉S ∧ c∈S ∧ d∉S) ∨ (a∉S ∧ b∈S ∧ c∉S ∧ d∈S)))
        {i j : Fin n} (hi : i∈S) (hj : j∈S) : G.Reachable i j := by
    …

    Mentions: OAI.PlanarL1.Columns.Consecutive

14. def OAI.PlanarL1.Topology.Drawing.carrier line 243
15. lemma OAI.PlanarL1.Topology.Drawing.point_mem_carrier line 247
16. lemma OAI.PlanarL1.Topology.Drawing.edge_mem_carrier line 250
17. lemma OAI.PlanarL1.Topology.Drawing.carrier_disjoint line 254
18. def OAI.PlanarL1.HeightTree.graph line 309
19. lemma OAI.PlanarL1.HeightTree.ancestor_path line 316
20. lemma OAI.PlanarL1.HeightTree.descendants_joined line 334
21. lemma OAI.PlanarL1.HeightTree.nondescendants_joined line 344
22. lemma OAI.PlanarL1.HeightTree.disk_prefix_connected line 363
23. lemma OAI.PlanarL1.HeightTree.layout_of_disk line 401

    Source documentation

    The exact leaf layout follows from a geometric disk drawing and disjoint complementary paths. This lemma does not assert the still-required disk surgery on the supplied planar drawing.

    lemma layout_of_disk [Fintype V] (D : Topology.Drawing T.graph)
        (hpoint : ∀ v, ‖D.point v‖≤1)
        (hedge : ∀ u v h t, ‖D.edge u v h t‖≤1)
        (hleaf : ∀ v, T.IsLeaf v → ‖D.point v‖=1)
        (P : SimpleGraph {v : V // T.IsLeaf v})
        (hheight : ∀ i j, P.Adj i j → T.height i.val=T.height j.val)
        (hmatch : ∀ i j k, P.Adj i j → P.Adj i k → j=k)
        (arc : ∀ i j, P.Adj i j → Path (D.point i.val) (D.point j.val))
        (hout : ∀ i j h t, 1≤‖arc i j h t‖)
        (hdis : ∀ 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'))) :
        ∃ (L : T.Layout (Fintype.card {v : V // T.IsLeaf v})),
    …

    Mentions: OAI.PlanarL1.Topology.Drawing