Surgery.lean`

60 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.PlanarL1.Topology.small_homothety_subset line 14

lemma OAI.PlanarL1.Topology.convex_radial_cut line 35

Source documentation

The radial exit from a convex neighbourhood. Both portions of the original segment are controlled; this is the actual cut used in a disk surgery.

lemma convex_radial_cut {S : Set E} (hS : Convex ℝ S) (h0 : S ∈ nhds (0:E))
    {p : E} (hp : p ∉ closure S) :
    ∃ t : ℝ, 0<t ∧ t<1 ∧ t•p ∈ frontier S ∧
      (∀ s : ℝ, 0 ≤ s → s < t → s • p ∈ interior S) ∧
      (∀ s : ℝ, t < s → s • p ∉ closure S) := by
…

lemma OAI.PlanarL1.Topology.convex_frontier_radial_interior line 58
lemma OAI.PlanarL1.Topology.convex_frontier_scaled_segment line 65

lemma OAI.PlanarL1.Topology.PLDrawing.ofRegions line 85

Source documentation

Polygonal edge regions with exactly the prescribed intersections give a literal simple polyline drawing, by finite loop erasure inside each region.

lemma ofRegions (p : V → ℂ) (hp : Function.Injective p)
    (R : ForwardDart G → Set ℂ)
    (hmem : ∀ d, p d.val.fst ∈ R d)
    (hjoin : ∀ d, PolygonallyJoined (R d) (p d.val.fst) (p d.val.snd))
    (hvertex : ∀ d v, p v ∈ R d → Incident d v)
    (hinter : ∀ d e, d≠e → ∀ z, z∈R d → z∈R e →
      (z=p d.val.fst ∨ z=p d.val.snd) ∧ (z=p e.val.fst ∨ z=p e.val.snd)) :
    ∃ Q : PLDrawing G, Q.point=p ∧ ∀ d, (Q.chain d).trace ⊆ R d := by
…

Mentions: OAI.PlanarL1.Topology.ForwardDart, OAI.PlanarL1.Topology.PolygonallyJoined, OAI.PlanarL1.Topology.PLDrawing.Incident, OAI.PlanarL1.Topology.PLDrawing

def OAI.PlanarL1.Topology.PLDrawing.radialPoint line 107
def OAI.PlanarL1.Topology.PLDrawing.radialRegion line 110
lemma OAI.PlanarL1.Topology.PLDrawing.radial_segment_subset line 122
lemma OAI.PlanarL1.Topology.PLDrawing.radialRegion_subset line 136
lemma OAI.PlanarL1.Topology.PLDrawing.radial_port_not_core line 145
lemma OAI.PlanarL1.Topology.PLDrawing.radialPoint_injective line 157
lemma OAI.PlanarL1.Topology.PLDrawing.radialPoint_in_tail line 174
lemma OAI.PlanarL1.Topology.PLDrawing.radialRegion_vertex line 191
lemma OAI.PlanarL1.Topology.PLDrawing.radialRegions_intersect line 211
lemma OAI.PlanarL1.Topology.PLDrawing.radialPoint_mem_region line 229
lemma OAI.PlanarL1.Topology.PLDrawing.radialRegion_joined line 242
lemma OAI.PlanarL1.Topology.PLDrawing.radial_leaf_ports line 265
Source documentation
All leaf tails may be cut at different positive radial coordinates. The result is an actual drawing, not merely a nonintersection promise.
```
lemma radial_leaf_ports : ∃ Q : PLDrawing G,
    Q.point=P.radialPoint B c t ∧ ∀ d, (Q.chain d).trace ⊆ P.radialRegion B c t d := by
…
```
Mentions: OAI.PlanarL1.Topology.PLDrawing
lemma OAI.PlanarL1.Topology.PLDrawing.radialRegion_subset_convex line 278
lemma OAI.PlanarL1.Topology.PolygonallyJoined.symm line 300
def OAI.PlanarL1.Topology.PLDrawing.movedPoint line 309
def OAI.PlanarL1.Topology.PLDrawing.movedRegion line 312
lemma OAI.PlanarL1.Topology.PLDrawing.movedPoint_injective line 322
lemma OAI.PlanarL1.Topology.PLDrawing.movedRegion_vertex line 341
lemma OAI.PlanarL1.Topology.PLDrawing.movedRegions_intersect line 358
lemma OAI.PlanarL1.Topology.PLDrawing.movedPoint_mem_region line 383
lemma OAI.PlanarL1.Topology.PLDrawing.movedRegion_joined line 398
lemma OAI.PlanarL1.Topology.PLDrawing.move_leaf line 415
Source documentation
Extending a drawn leaf along a polygonal region disjoint from the rest of the drawing preserves a literal polyline drawing and the exact vertices.
```
lemma move_leaf (hjoin : PolygonallyJoined S (P.point v) q) :
    ∃ Q : PLDrawing G, Q.point=P.movedPoint v q ∧
      ∀ d, (Q.chain d).trace ⊆ P.movedRegion v S d := by
…
```
Mentions: OAI.PlanarL1.Topology.PolygonallyJoined, OAI.PlanarL1.Topology.PLDrawing
lemma OAI.PlanarL1.Topology.convex_segment_cut line 438
lemma OAI.PlanarL1.Topology.convex_frontier_segment line 461

lemma OAI.PlanarL1.Topology.capsule_avoiding_ports line 476

Source documentation

A convex capsule around one radial arm avoids all other ports and every closed external obstacle. This is the merging disk, not an assumed regular neighbourhood of an embedded tree.

lemma capsule_avoiding_ports {ι : Type*} [Finite ι] (p : ι → ℂ)
    (hinj : Function.Injective p) {B : Set ι} {v : ι} (hv : v∈B)
    {S F : Set ℂ} (hS : Convex ℝ S) (h0 : S∈nhds (0:ℂ))
    (hport : ∀ w∈B, p w∈frontier S) (hF : IsClosed F)
    (hdisj : Disjoint (segment ℝ 0 (p v)) F) :
    ∃ T : Set ℂ, Convex ℝ T ∧ IsOpen T ∧ Bornology.IsBounded T ∧
      segment ℝ 0 (p v) ⊆ T ∧ Disjoint (closure T) F ∧
      ∀ w∈B, w≠v → p w∉closure T := by
…

lemma OAI.PlanarL1.Topology.capsule_radial_data line 499

Source documentation

Radial cuts of all unselected ports, after a sufficiently small homothety of the bounded old disk. The selected port stays in the interior of the new disk; it will be extended along the next exterior straight piece.

lemma capsule_radial_data {ι : Type*} (p : ι → ℂ) {B : Set ι} {v : ι}
    {S T : Set ℂ} (hSbound : Bornology.IsBounded S)
    (hpoint : ∀ w, p w∈closure S)
    (hT : Convex ℝ T) (hTop : IsOpen T) (hT0 : (0:ℂ)∈T)
    (hout : ∀ w∈B, w≠v → p w∉closure T) :
    ∃ (c : ℝ) (t : ι → ℝ), 0<c ∧ c<1 ∧
      (fun z : ℂ => c•z) '' closure S ⊆ T ∧ t v=1 ∧
      (∀ w∈B, c<t w ∧ t w≤1) ∧
      (∀ w∈B, w≠v → t w•p w∈frontier T) ∧
      (∀ w∈B, w≠v → ∀ s : ℝ, t w < s → s•p w∉closure T) := by
…

def OAI.PlanarL1.Topology.PLDrawing.forward line 549
lemma OAI.PlanarL1.Topology.PLDrawing.forward_endpoints line 554
lemma OAI.PlanarL1.Topology.PLDrawing.forward_symm line 560
def OAI.PlanarL1.Topology.PLDrawing.region line 569
lemma OAI.PlanarL1.Topology.PLDrawing.region_eq line 572
lemma OAI.PlanarL1.Topology.PLDrawing.region_symm line 575
lemma OAI.PlanarL1.Topology.PLDrawing.region_joined line 581
lemma OAI.PlanarL1.Topology.PLDrawing.region_start line 588
lemma OAI.PlanarL1.Topology.PLDrawing.region_end line 595
lemma OAI.PlanarL1.Topology.PLDrawing.region_vertex line 598
lemma OAI.PlanarL1.Topology.PLDrawing.region_intersect line 606
lemma OAI.PlanarL1.Topology.PLDrawing.ofSymmetricRegions line 626
def OAI.PlanarL1.Topology.leafExtension line 647
Source documentation
Adding finitely many new leaves to one vertex; no geometric or metric conclusion is included in this graph definition.
```
def leafExtension {V W : Type} (G : SimpleGraph V) (v : V) : SimpleGraph (V⊕W) where
…
```
def OAI.PlanarL1.Topology.PLDrawing.starPoint line 663
def OAI.PlanarL1.Topology.PLDrawing.starRegion line 665

lemma OAI.PlanarL1.Topology.PLDrawing.attachLeaves line 673

Source documentation

A finite star of genuinely disjoint polygonal arms can be attached at an existing vertex while retaining every old vertex and edge region.

lemma attachLeaves
    (hq : ∀ w, q w≠P.point v)
    (hstart : ∀ w, P.point v∈A w) (hend : ∀ w, q w∈A w)
    (hjoin : ∀ w, PolygonallyJoined (A w) (P.point v) (q w))
    (hvertex : ∀ w u, P.point u∈A w → u=v)
    (hdisj : ∀ w w', w≠w' → ∀ z, z∈A w → z∈A w' → z=P.point v)
    (hold : ∀ w u x, G.Adj u x → ∀ z, z∈A w → z∈P.region u x → z=P.point v) :
    ∃ Q : PLDrawing (leafExtension (W := W) G v), Q.point=P.starPoint q ∧
…

Mentions: OAI.PlanarL1.Topology.PolygonallyJoined, OAI.PlanarL1.Topology.PLDrawing, OAI.PlanarL1.Topology.leafExtension

lemma OAI.PlanarL1.Topology.PolygonallyJoined.affine line 800
def OAI.PlanarL1.Topology.SegmentChain.affine line 813
lemma OAI.PlanarL1.Topology.SegmentChain.affine_trace line 819
lemma OAI.PlanarL1.Topology.SegmentChain.trace_compact line 822
lemma OAI.PlanarL1.Topology.SegmentChain.affine_simple line 829
def OAI.PlanarL1.Topology.SegmentChain.reverse line 844
lemma OAI.PlanarL1.Topology.SegmentChain.reverse_trace line 853
def OAI.PlanarL1.Topology.SegmentChain.prepend line 877
lemma OAI.PlanarL1.Topology.SegmentChain.prepend_trace line 889
def OAI.PlanarL1.Topology.PLDrawing.affine line 915
lemma OAI.PlanarL1.Topology.PLDrawing.affine_point line 939
lemma OAI.PlanarL1.Topology.PLDrawing.affine_trace line 940
lemma OAI.PlanarL1.Topology.PLDrawing.region_compact line 944