OAI/Combinatorics/PlanarL1/Polygonal.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PlanarL1.Topology.SegmentChain line 13

   Source documentation

   A finite segment chain, represented by its value at every integer; only the first length + 1 values are used.

   structure SegmentChain (S : Set E) (x y : E) (length : ℕ) where
   …

2. def OAI.PlanarL1.Topology.SegmentChain.nil line 22
3. def OAI.PlanarL1.Topology.SegmentChain.append line 28
4. def OAI.PlanarL1.Topology.SegmentChain.eraseLoop line 40

   Source documentation

   Remove a closed loop in a segment chain.

   noncomputable def eraseLoop (i j : ℕ) (hij : i<j) (hjn : j≤n)
       (heq : P.vertex i=P.vertex j) : SegmentChain S x y (n-j+i) where
   …

   Mentions: OAI.PlanarL1.Topology.SegmentChain

5. def OAI.PlanarL1.Topology.SegmentChain.shortcut line 68

   Source documentation

   Replace several successive edges by one segment already known to lie in the permitted set.

   noncomputable def shortcut (i j : ℕ) (hij : i<j) (hjn : j≤n)
       (hseg : segment ℝ (P.vertex i) (P.vertex j) ⊆ S) :
       SegmentChain S x y (n-j+i+1) where
   …

   Mentions: OAI.PlanarL1.Topology.SegmentChain

6. def OAI.PlanarL1.Topology.SegmentChain.shortcutAt line 92

   Source documentation

   Delete the part between two intersecting, nonadjacent segments.

   noncomputable def shortcutAt (i j : ℕ) (hij : i<j) (hjn : j<n) (z : E)
       (hzi : z ∈ segment ℝ (P.vertex i) (P.vertex (i+1)))
       (hzj : z ∈ segment ℝ (P.vertex j) (P.vertex (j+1))) :
       SegmentChain S x y (n-j+i+1) where
   …

   Mentions: OAI.PlanarL1.Topology.SegmentChain

7. lemma OAI.PlanarL1.Topology.PolygonallyJoined.exists_segmentChain line 125
8. lemma OAI.PlanarL1.Topology.collinear_segment_union line 134

   Source documentation

   A collinear broken segment covers the direct segment.

   lemma collinear_segment_union {a b c : E} (h : Collinear ℝ ({a,b,c} : Set E)) :
       segment ℝ a c ⊆ segment ℝ a b ∪ segment ℝ b c := by
   …

9. lemma OAI.PlanarL1.Topology.collinear_of_adjacent_overlap line 155

   Source documentation

   Adjacent non-collinear segments have no intersection except their common endpoint. This elementary fact supplies loop erasure without a Jordan theorem.

   lemma collinear_of_adjacent_overlap {a b c z : E}
       (hz : z ∈ segment ℝ a b) (hz' : z ∈ segment ℝ b c) (hne : z≠b) :
       Collinear ℝ ({a,b,c} : Set E) := by
   …

10. def OAI.PlanarL1.Topology.SegmentChain.IsMinimal line 177
11. def OAI.PlanarL1.Topology.SegmentChain.IsSimple line 180
12. lemma OAI.PlanarL1.Topology.SegmentChain.minimal_vertex_injective line 187
13. lemma OAI.PlanarL1.Topology.SegmentChain.minimal_nonadjacent line 198
14. lemma OAI.PlanarL1.Topology.SegmentChain.minimal_adjacent line 206
15. lemma OAI.PlanarL1.Topology.SegmentChain.minimal_simple line 217
16. lemma OAI.PlanarL1.Topology.PolygonallyJoined.exists_simple_segmentChain line 227

    Source documentation

    Every finite polygonal connection contains a simple finite polygonal connection with the same endpoints and no larger trace.

    lemma PolygonallyJoined.exists_simple_segmentChain {S : Set E} {x y : E}
        (h : PolygonallyJoined S x y) :
        ∃ n, ∃ P : SegmentChain S x y n, P.IsSimple := by
    …

    Mentions: OAI.PlanarL1.Topology.PolygonallyJoined, OAI.PlanarL1.Topology.SegmentChain

17. lemma OAI.PlanarL1.Topology.PolygonallyJoined.mono line 243
18. def OAI.PlanarL1.Topology.SegmentChain.trace line 253

    Source documentation

    The finite geometric trace, including the degenerate chain's endpoint.

    def trace : Set E := {x} ∪ ⋃ i : Fin n, segment ℝ (P.vertex i) (P.vertex (i+1))

19. lemma OAI.PlanarL1.Topology.SegmentChain.trace_subset line 255
20. lemma OAI.PlanarL1.Topology.SegmentChain.vertex_mem_trace line 261
21. lemma OAI.PlanarL1.Topology.SegmentChain.start_mem_trace line 269
22. lemma OAI.PlanarL1.Topology.SegmentChain.finish_mem_trace line 270
23. lemma OAI.PlanarL1.Topology.radial_segment_dist_le line 276
24. def OAI.PlanarL1.Topology.Drawing.portVertex line 286

    Source documentation

    A boundary port and its incident vertex.

    def portVertex (d : ForwardDart G) (b : Bool) : V := if b then d.val.snd else d.val.fst

    Mentions: OAI.PlanarL1.Topology.ForwardDart

25. def OAI.PlanarL1.Topology.Drawing.port line 287
26. def OAI.PlanarL1.Topology.Drawing.head line 289
27. lemma OAI.PlanarL1.Topology.Drawing.port_sphere line 292
28. lemma OAI.PlanarL1.Topology.Drawing.head_dist line 298
29. lemma OAI.PlanarL1.Topology.Drawing.ports_distinct line 302
30. lemma OAI.PlanarL1.Topology.Drawing.heads_intersect line 314
31. lemma OAI.PlanarL1.Topology.Drawing.vertex_mem_head line 334
32. lemma OAI.PlanarL1.Topology.Drawing.head_mem_obstacle line 344
33. def OAI.PlanarL1.Topology.Drawing.edgeRegion line 353
34. lemma OAI.PlanarL1.Topology.Drawing.region_joined line 356
35. lemma OAI.PlanarL1.Topology.Drawing.region_vertex line 366
36. lemma OAI.PlanarL1.Topology.Drawing.regions_intersect line 376
37. def OAI.PlanarL1.Topology.SegmentChain.mapSet line 415
38. lemma OAI.PlanarL1.Topology.SegmentChain.mapSet_simple line 421
39. lemma OAI.PlanarL1.Topology.SegmentChain.mapSet_trace line 422
40. structure OAI.PlanarL1.Topology.PLDrawing line 428

    Source documentation

    A literal finite polyline drawing. Simplicity is a proved property of the finite segment chains, not an added planarity promise.

    structure PLDrawing {V : Type} [LinearOrder V] (G : SimpleGraph V) where
    …

41. lemma OAI.PlanarL1.Topology.Drawing.polygonal line 440

    Source documentation

    Simultaneous polygonalization of a finite topological graph drawing. The original positions of all vertices are retained.

    lemma Drawing.polygonal {V : Type} [Fintype V] [LinearOrder V] {G : SimpleGraph V}
        (D : Drawing G) : ∃ P : PLDrawing G, P.point=D.point := by
    …

    Mentions: OAI.PlanarL1.Topology.Drawing, OAI.PlanarL1.Topology.PLDrawing

42. lemma OAI.PlanarL1.Topology.polygonal_of_planar line 460
43. lemma OAI.PlanarL1.Topology.convex_frontier_radial_injective line 477

    Source documentation

    Boundary points of a convex neighbourhood have a unique positive radial coordinate. This will keep the extended leaf ports disjoint when shrinking an embedded finite tree inside a convex merging region.

    lemma convex_frontier_radial_injective {S : Set E} (hS : Convex ℝ S)
        (h0 : S ∈ nhds (0:E)) {p q : E} (hp : p ∈ frontier S) (hq : q ∈ frontier S)
        {s t : ℝ} (hs : 0<s) (ht : 0<t) (he : s • p=t • q) : s=t ∧ p=q := by
    …

44. lemma OAI.PlanarL1.Topology.convex_frontier_tails_disjoint line 491

    Source documentation

    The outer radial tails from different ports never meet, including their endpoints.

    lemma convex_frontier_tails_disjoint {S : Set E} (hS : Convex ℝ S)
        (h0 : S ∈ nhds (0:E)) {p q : E} (hp : p ∈ frontier S) (hq : q ∈ frontier S)
        (hpq : p≠q) {c : ℝ} (hc : 0<c) (hc1 : c≤1) :
        Disjoint (segment ℝ (c•p) p) (segment ℝ (c•q) q) := by
    …

45. lemma OAI.PlanarL1.Topology.convex_frontier_tail_core line 509
46. lemma OAI.PlanarL1.Topology.convex_tube_avoiding line 535

    Source documentation

    A straight selected tree piece has an arbitrarily thin bounded convex merging region avoiding every closed nonincident obstacle.

    lemma convex_tube_avoiding {a b : ℂ} {F : Set ℂ} (hF : IsClosed F)
        (hdisj : Disjoint (segment ℝ a b) F) :
        ∃ S : Set ℂ, Convex ℝ S ∧ IsOpen S ∧ Bornology.IsBounded S ∧
          segment ℝ a b ⊆ S ∧ Disjoint (closure S) F := by
    …

47. lemma OAI.PlanarL1.Topology.image_segment_smul line 555
48. lemma OAI.PlanarL1.Topology.PolygonallyJoined.smul line 562
49. lemma OAI.PlanarL1.Topology.SegmentChain.joined_trace line 572
50. def OAI.PlanarL1.Topology.PLDrawing.Incident line 588
51. lemma OAI.PlanarL1.Topology.PLDrawing.leaf_incident_unique line 590
52. def OAI.PlanarL1.Topology.PLDrawing.expandedPoint line 608
53. def OAI.PlanarL1.Topology.PLDrawing.portTail line 611
54. def OAI.PlanarL1.Topology.PLDrawing.expandedRegion line 613
55. lemma OAI.PlanarL1.Topology.PLDrawing.port_not_core line 624
56. lemma OAI.PlanarL1.Topology.PLDrawing.expandedPoint_injective line 636
57. lemma OAI.PlanarL1.Topology.PLDrawing.newpoint_in_tail line 650
58. lemma OAI.PlanarL1.Topology.PLDrawing.newpoint_in_core line 665
59. lemma OAI.PlanarL1.Topology.PLDrawing.expandedRegion_vertex line 679
60. lemma OAI.PlanarL1.Topology.PLDrawing.different_core_tail line 694
61. lemma OAI.PlanarL1.Topology.PLDrawing.different_tails line 707
62. lemma OAI.PlanarL1.Topology.PLDrawing.expandedRegions_intersect line 716
63. lemma OAI.PlanarL1.Topology.PLDrawing.expandedPoint_mem_region line 751
64. lemma OAI.PlanarL1.Topology.PLDrawing.expandedRegion_joined line 764
65. lemma OAI.PlanarL1.Topology.PLDrawing.expand_leaf_ports line 789

    Source documentation

    Inside a convex merging region, shrink the complete drawn core but retain all its distinct leaf ports. Extending each leaf radially introduces no intersections. The result is again an actual finite polyline drawing.

    lemma expand_leaf_ports : ∃ Q : PLDrawing G,
        Q.point=P.expandedPoint B c ∧ ∀ d, (Q.chain d).trace ⊆ P.expandedRegion B c d := by
    …

    Mentions: OAI.PlanarL1.Topology.PLDrawing