OAI/Combinatorics/PlanarL1/Retubing.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarL1.Topology.frontier_outward_segment line 12
2. lemma OAI.PlanarL1.Topology.scalar_segment line 26
3. lemma OAI.PlanarL1.Topology.radial_outer_tail line 35
4. def OAI.PlanarL1.Topology.PLDrawing.retubePoint line 45
5. def OAI.PlanarL1.Topology.PLDrawing.retubeRegion line 48
6. lemma OAI.PlanarL1.Topology.PLDrawing.retube_extend line 55

   Source documentation

   Compress a genuine finite drawing into a new convex tube and extend one leaf along a segment external to the old disk. Every other exposed leaf is cut exactly at the new frontier. The exterior residual tails meet the new closed disk only at their new ports.

   lemma retube_extend {S T : Set ℂ} {B : Set V} {v : V} {q : ℂ}
       (hS : Convex ℝ S) (hS0 : S∈nhds (0:ℂ)) (hSb : Bornology.IsBounded S)
       (hpoint : ∀ w, P.point w∈closure S)
       (htrace : ∀ d, (P.chain d).trace ⊆ closure S)
       (hport : ∀ w∈B, P.point w∈frontier S)
       (hleaf : ∀ w∈B, ∀ a b, G.Adj w a → G.Adj w b → a=b)
       (hv : v∈B) (hT : Convex ℝ T) (hTop : IsOpen T) (hT0 : (0:ℂ)∈T)
       (hTv : P.point v∈T) (hqT : q∈closure T)
       (hout : ∀ w∈B, w≠v → P.point w∉closure T)
       (hext : ∀ z, z∈segment ℝ (P.point v) q → z∈closure S → z=P.point v) :
       ∃ (c : ℝ) (t : V → ℝ) (Q : PLDrawing G), 0<c ∧ c<1 ∧ t v=1 ∧
         (∀ w∈B, c<t w ∧ t w≤1) ∧ Q.point=P.retubePoint B c t v q ∧
   …

   Mentions: OAI.PlanarL1.Topology.PLDrawing

7. lemma OAI.PlanarL1.Topology.PLDrawing.radialRegion_old line 158
8. structure OAI.PlanarL1.Topology.PLDrawing.PortMove line 178

   Source documentation

   The exact geometric output needed when retubing a tree with exterior stems. The old disk may be discarded, but no new curve leaves it except along the selected stem segment.

   structure PortMove (p : V → ℂ) (Q : PLDrawing G) (B : Set V) (v : V) (q : ℂ) (S T : Set ℂ) : Prop where
   …

   Mentions: OAI.PlanarL1.Topology.PLDrawing

9. lemma OAI.PlanarL1.Topology.PLDrawing.retube_controlled line 193
10. lemma OAI.PlanarL1.Topology.PLDrawing.affine_image_closure line 284
11. lemma OAI.PlanarL1.Topology.PLDrawing.affine_image_frontier line 287
12. lemma OAI.PlanarL1.Topology.PLDrawing.PortMove.affine line 291
13. lemma OAI.PlanarL1.Topology.PLDrawing.retube_at line 335
14. structure OAI.PlanarL1.Topology.PortFrame line 404

    Source documentation

    Released radial port tails; unlike PortMove this does not prescribe the selected route, which may already have passed through several bends.

    structure PortFrame (p a : V → ℂ) (B : Set V) (v : V) (q : ℂ) (S T : Set ℂ) : Prop where
    …

15. lemma OAI.PlanarL1.Topology.PortFrame.ofMove line 416
16. lemma OAI.PlanarL1.Topology.PortFrame.repoint line 421
17. structure OAI.PlanarL1.Topology.ExteriorPorts line 435

    Source documentation

    Actual disjoint exterior polygonal stems, not a promised contour order.

    structure ExteriorPorts (p target : V → ℂ) (B : Set V) (S : Set ℂ) where
    …

18. lemma OAI.PlanarL1.Topology.ExteriorPorts.end_mem line 446
19. lemma OAI.PlanarL1.Topology.ExteriorPorts.tail_disjoint_region line 454
20. def OAI.PlanarL1.Topology.ExteriorPorts.updatedRegion line 465
21. def OAI.PlanarL1.Topology.ExteriorPorts.update line 470

    Source documentation

    Replacing one residual stem, and adjoining the released radial tails to all other stems, preserves literal disjoint exterior routes.

    noncomputable def update {a : V → ℂ} {v : V} {q : ℂ} {T U : Set ℂ}
        (h : PortFrame p a B v q S T) (hinj : Function.Injective p)
        (hport : ∀ w∈B, p w∈frontier S) (hv : v∈B)
        (hout : ∀ w∈B, w≠v → Disjoint (closure T) (E.region w))
        (hU : IsCompact U) (hqU : q∈U) (hUsub : U ⊆ E.region v)
        (hUin : ∀ z∈U, z∈closure T → z=q)
        (hUjoin : PolygonallyJoined U q (target v)) : ExteriorPorts a target B T where
    …

    Mentions: OAI.PlanarL1.Topology.PortFrame, OAI.PlanarL1.Topology.PolygonallyJoined, OAI.PlanarL1.Topology.ExteriorPorts

22. def OAI.PlanarL1.Topology.SegmentChain.tail line 540
23. lemma OAI.PlanarL1.Topology.SegmentChain.tail_trace line 546
24. lemma OAI.PlanarL1.Topology.SegmentChain.tail_simple line 566
25. lemma OAI.PlanarL1.Topology.SegmentChain.head_tail_intersection line 578
26. lemma OAI.PlanarL1.Topology.SegmentChain.first_ne line 586
27. lemma OAI.PlanarL1.Topology.SegmentChain.start_not_tail line 592
28. lemma OAI.PlanarL1.Topology.SegmentChain.finish_not_first line 596
29. def OAI.PlanarL1.Topology.SegmentChain.cutFirst line 607
30. lemma OAI.PlanarL1.Topology.SegmentChain.cutFirst_trace line 620
31. lemma OAI.PlanarL1.Topology.SegmentChain.cutFirst_subset line 625
32. lemma OAI.PlanarL1.Topology.SegmentChain.cutFirst_simple line 629