OAI/Combinatorics/PlanarL1/Growth.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   After processing a frontier vertex, the old remaining ports and all its new children are the frontier.

   def starPorts (B : Set V) (v : V) : Set (V⊕W) :=
   …

2. lemma OAI.PlanarL1.Topology.DiskCore.grow_star line 22
3. lemma OAI.PlanarL1.HeightTree.parent_ne line 218
4. lemma OAI.PlanarL1.HeightTree.step_ne line 224
5. def OAI.PlanarL1.HeightTree.ParentClosed line 228

   Source documentation

   Vertices already absorbed into the disk form a parent-closed set.

   def ParentClosed (S : Finset V) : Prop := ∀ v∈S, T.parent v∈S

6. def OAI.PlanarL1.HeightTree.Frontier line 230
7. def OAI.PlanarL1.HeightTree.Scope line 232
8. lemma OAI.PlanarL1.HeightTree.frontier_ne_root line 234
9. lemma OAI.PlanarL1.HeightTree.scope_parent line 238
10. lemma OAI.PlanarL1.HeightTree.frontier_neighbor line 241
11. lemma OAI.PlanarL1.HeightTree.frontier_leaf line 247
12. lemma OAI.PlanarL1.HeightTree.child_out line 254
13. lemma OAI.PlanarL1.HeightTree.insert_closed line 261
14. lemma OAI.PlanarL1.HeightTree.frontier_insert line 269
15. lemma OAI.PlanarL1.HeightTree.scope_insert line 283
16. lemma OAI.PlanarL1.HeightTree.old_child_adj line 302
17. lemma OAI.PlanarL1.HeightTree.children_not_adj line 312
18. def OAI.PlanarL1.HeightTree.extensionMap line 318
19. lemma OAI.PlanarL1.HeightTree.extensionMap_injective line 322
20. def OAI.PlanarL1.HeightTree.extensionEquiv line 337
21. lemma OAI.PlanarL1.HeightTree.extension_graph line 350
22. lemma OAI.PlanarL1.HeightTree.extension_ports line 371
23. lemma OAI.PlanarL1.Topology.PLDrawing.pullback line 395
24. def OAI.PlanarL1.Topology.ExteriorPorts.retarget line 410
25. lemma OAI.PlanarL1.Topology.DiskCore.region_mem line 423
26. lemma OAI.PlanarL1.Topology.DiskCore.pullback line 429

    Source documentation

    Relabel an actual core and all exterior paths along an injective graph map. No drawing or disk existence is assumed beyond the supplied core.

    lemma pullback (E : ExteriorPorts C.drawing.point target B C.disk)
        (f : W → V) (hf : Function.Injective f)
        (hG : ∀ u v, H.Adj u v → G.Adj (f u) (f v))
        {B' : Set W} (hB : ∀ w∈B', f w∈B) :
        ∃ C' : DiskCore H B', ∃ E' : ExteriorPorts C'.drawing.point (target ∘ f) B' C'.disk,
          C'.disk=C.disk ∧ (∀ w, C'.drawing.point w=C.drawing.point (f w)) ∧
          (∀ w, E'.region w=E.region (f w)) := by
    …

    Mentions: OAI.PlanarL1.Topology.ExteriorPorts, OAI.PlanarL1.Topology.DiskCore

27. def OAI.PlanarL1.Topology.PLDrawing.carrier line 461
28. lemma OAI.PlanarL1.Topology.PLDrawing.point_mem_carrier line 464
29. lemma OAI.PlanarL1.Topology.PLDrawing.region_mem_carrier line 467
30. lemma OAI.PlanarL1.Topology.PLDrawing.carrier_mono line 471
31. lemma OAI.PlanarL1.Topology.PLDrawing.carrier_compact line 480
32. lemma OAI.PlanarL1.Topology.PLDrawing.region_adj line 484
33. lemma OAI.PlanarL1.Topology.PLDrawing.point_carrier_iff line 489
34. lemma OAI.PlanarL1.Topology.PLDrawing.region_carrier_intersection line 500
35. lemma OAI.PlanarL1.Topology.PLDrawing.carrier_disjoint line 521
36. lemma OAI.PlanarL1.Topology.PLDrawing.region_simple_chain line 536
37. def OAI.PlanarL1.HeightTree.outside line 556

    Source documentation

    The raw unprocessed drawing is a fixed closed obstacle at each stage.

    def outside (S : Finset V) : Set ℂ := P.carrier {v | v∉S}

38. lemma OAI.PlanarL1.HeightTree.outside_closed line 558
39. lemma OAI.PlanarL1.HeightTree.outside_insert_subset line 562
40. lemma OAI.PlanarL1.HeightTree.point_outside_iff line 567
41. structure OAI.PlanarL1.HeightTree.Growth line 572

    Source documentation

    A partially swallowed tree, retaining real residual stems to the original frontier vertices in the supplied polygonal drawing.

    structure Growth (S : Finset V) where
    …

42. lemma OAI.PlanarL1.HeightTree.Growth.advance line 584
43. lemma OAI.PlanarL1.HeightTree.singleton_closed line 680
44. lemma OAI.PlanarL1.HeightTree.frontier_root_iff line 686
45. lemma OAI.PlanarL1.HeightTree.scope_root_iff line 690
46. def OAI.PlanarL1.HeightTree.rootMap line 694
47. lemma OAI.PlanarL1.HeightTree.rootMap_injective line 696
48. def OAI.PlanarL1.HeightTree.rootEquiv line 706
49. lemma OAI.PlanarL1.HeightTree.root_graph line 718
50. lemma OAI.PlanarL1.HeightTree.root_ports line 735
51. def OAI.PlanarL1.Topology.singletonDrawing line 756
52. lemma OAI.PlanarL1.Topology.star_core line 767

    Source documentation

    The first enclosing disk cuts each outgoing polygonal arm once, leaving its entire residual trace outside.

    lemma star_core (y : ℂ) (child : W → ℂ) (n : W → ℕ)
        (P : ∀ w, SegmentChain Set.univ y (child w) (n w+1))
        (hP : ∀ w, (P w).IsSimple)
        (hPP : ∀ w w', w≠w' → ∀ z∈(P w).trace, z∈(P w').trace → z=y)
        {K : Set ℂ} (hK : IsClosed K) (hyK : y∉K)
        (hPK : ∀ w, ∀ z∈(P w).trace, z∈K → z=child w) :
        ∃ C : DiskCore (leafExtension (W := W) (⊥ : SimpleGraph PUnit) PUnit.unit)
    …

    Mentions: OAI.PlanarL1.Topology.SegmentChain, OAI.PlanarL1.Topology.DiskCore, OAI.PlanarL1.Topology.leafExtension

53. lemma OAI.PlanarL1.HeightTree.initial_growth line 886