Drawing.lean`

41 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.PlanarL1.Topology.Drawing line 13
Source documentation
The literal topological drawing, with its coordinates identified with the complex plane. No polygonal or combinatorial planarity assumption is added.
```
structure Drawing {V : Type} (G : SimpleGraph V) where
…
```
lemma OAI.PlanarL1.Topology.drawing_of_planar line 24
lemma OAI.PlanarL1.Topology.Drawing.point_on_edge_iff line 41
def OAI.PlanarL1.Topology.Drawing.excludedTimes line 62
Source documentation
Away from the first/last third of an incident edge, every vertex is uniformly separated from that edge. The set is closed even at both cutoffs.
```
def excludedTimes (w : V) (d : G.Dart) : Set unitInterval :=
…
```
lemma OAI.PlanarL1.Topology.Drawing.excludedTimes_closed line 65
lemma OAI.PlanarL1.Topology.Drawing.excludedTimes_avoid line 73
def OAI.PlanarL1.Topology.Drawing.forbidden line 87
Source documentation
A compact forbidden set for a vertex disk: other vertices and the parts of every drawn edge that must stay outside that disk.
```
def forbidden (w : V) : Set ℂ :=
…
```
lemma OAI.PlanarL1.Topology.Drawing.forbidden_compact line 91
lemma OAI.PlanarL1.Topology.Drawing.forbidden_avoid line 99
lemma OAI.PlanarL1.Topology.Drawing.vertex_disk line 106
lemma OAI.PlanarL1.Topology.Drawing.uniform_vertex_disks line 118
Source documentation
One common positive radius works for all vertices; arbitrary edge oscillations and arbitrary straight-line distances between drawn vertices are allowed. This radius is topological auxiliary data, not a metric edge scale.
```
lemma uniform_vertex_disks :
    ∃ r>0, ∀ w z, z ∈ D.forbidden w → 5*r<dist (D.point w) z := by
…
```
lemma OAI.PlanarL1.Topology.path_lastExit line 137
Source documentation
Last exit from a closed disk before a specified later time. This works for arbitrary continuous paths, including paths which oscillate infinitely near their endpoint. No local straightness of a topological arc is assumed.
```
lemma path_lastExit {X : Type*} [MetricSpace X] {x y : X} (p : Path x y)
    {b r : ℝ} (hb : 0<b) (hr : 0<r)
    (hout : r<dist (p.extend b) x) :
    ∃ a : ℝ, 0<a ∧ a<b ∧ dist (p.extend a) x=r ∧
      ∀ t, a<t → t≤b → r<dist (p.extend t) x := by
…
```
lemma OAI.PlanarL1.Topology.path_trimStart line 162
lemma OAI.PlanarL1.Topology.Drawing.edge_mem_forbidden line 184
lemma OAI.PlanarL1.Topology.Drawing.point_mem_forbidden line 189
structure OAI.PlanarL1.Topology.Drawing.EdgeTrim line 194
Source documentation
Truncate one actual drawn edge outside disjoint small vertex disks. The middle arc stays outside every disk, with equality only at its own ends.
```
structure EdgeTrim (r : ℝ) (d : G.Dart) where
…
```
lemma OAI.PlanarL1.Topology.Drawing.edgeTrim_nonempty line 208
lemma OAI.PlanarL1.Topology.Drawing.EdgeTrim.first_lt_last line 256
lemma OAI.PlanarL1.Topology.Drawing.EdgeTrim.middle_outside line 262
lemma OAI.PlanarL1.Topology.Drawing.EdgeTrim.middle_strict line 280
def OAI.PlanarL1.Topology.PolygonallyJoined line 305
Source documentation
A finite chain of straight segments contained in a specified set.
```
def PolygonallyJoined (S : Set E) (x y : E) : Prop :=
…
```
lemma OAI.PlanarL1.Topology.polygonallyJoined_of_path line 308

lemma OAI.PlanarL1.Topology.PolygonallyJoined.exists_chain line 338

Source documentation

Polygonal connectivity has literal finite-list witnesses.

lemma PolygonallyJoined.exists_chain {S : Set E} {x y : E}
    (h : PolygonallyJoined S x y) :
    ∃ l : List E, (x::l).IsChain (fun a b => segment ℝ a b ⊆ S) ∧
      (x::l).getLast (by simp)=y := by
…

Mentions: OAI.PlanarL1.Topology.PolygonallyJoined

lemma OAI.PlanarL1.Topology.finite_disjoint_open_neighborhoods line 347

Source documentation

Disjoint compact arcs can be simultaneously thickened, while avoiding separate closed obstacles. No finiteness or regularity of the arcs themselves beyond compactness is used.

lemma finite_disjoint_open_neighborhoods {ι X : Type*} [Fintype ι] [MetricSpace X]
    (K F : ι → Set X) (hK : ∀ i, IsCompact (K i)) (hF : ∀ i, IsClosed (F i))
    (hKF : ∀ i, Disjoint (K i) (F i)) (hKK : Pairwise (fun i j => Disjoint (K i) (K j))) :
    ∃ U : ι → Set X, (∀ i, IsOpen (U i) ∧ K i ⊆ U i ∧ Disjoint (U i) (F i)) ∧
      Pairwise (fun i j => Disjoint (U i) (U j)) := by
…

lemma OAI.PlanarL1.Topology.radial_segment_boundary line 383
Source documentation
On a radial segment, the endpoint is the only point at its maximal radius. This is valid in every real normed space, without strict convexity.
```
lemma radial_segment_boundary {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {x y z : E} {r : ℝ} (hr : 0<r) (hy : dist y x=r)
    (hz : z ∈ segment ℝ x y) (hlo : r≤dist z x) : z=y := by
…
```
lemma OAI.PlanarL1.Topology.compact_segment_complex line 394

lemma OAI.PlanarL1.Topology.radial_heads_intersect line 399

Source documentation

Distinct radial heads on the same sphere intersect only at their center.

lemma radial_heads_intersect {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {x y w z : E} {r : ℝ} (hr : 0<r) (hy : dist y x=r) (hw : dist w x=r)
    (hne : y≠w) (hz : z ∈ segment ℝ x y) (hz' : z ∈ segment ℝ x w) : z=x := by
…

def OAI.PlanarL1.Topology.ForwardDart line 420
Source documentation
Choosing only the forward dart avoids treating the two independently supplied oriented parametrizations as one geometric edge.
```
def ForwardDart {V : Type} [LinearOrder V] (G : SimpleGraph V) :=
…
```
instance OAI.PlanarL1.Topology.ForwardDart.(instance at line 426) line 426
lemma OAI.PlanarL1.Topology.ForwardDart.eq_of_endpoints line 428
def OAI.PlanarL1.Topology.Drawing.EdgeTrim.middle line 444
lemma OAI.PlanarL1.Topology.Drawing.EdgeTrim.middle_range line 448
lemma OAI.PlanarL1.Topology.Drawing.EdgeTrim.middle_compact line 452
lemma OAI.PlanarL1.Topology.Drawing.EdgeTrim.middle_avoid_vertices line 455
lemma OAI.PlanarL1.Topology.Drawing.EdgeTrim.middle_radial_head line 461
lemma OAI.PlanarL1.Topology.Drawing.EdgeTrim.middle_radial_tail line 476
lemma OAI.PlanarL1.Topology.Drawing.forward_middles_disjoint line 495
def OAI.PlanarL1.Topology.Drawing.middleObstacle line 510
Source documentation
Obstacles for the middle of an edge: all vertices and the radial heads of every other unoriented edge.
```
noncomputable def middleObstacle (d : ForwardDart G) : Set ℂ :=
…
```
Mentions: OAI.PlanarL1.Topology.ForwardDart
lemma OAI.PlanarL1.Topology.Drawing.middleObstacle_closed line 517
lemma OAI.PlanarL1.Topology.Drawing.middleObstacle_disjoint line 523

lemma OAI.PlanarL1.Topology.Drawing.polygonal_middles line 540

Source documentation

Every trimmed edge can be replaced by a literal finite segment chain, inside mutually disjoint open tubes avoiding all other edge heads and all vertices. This is the needed simultaneous polygonalization step.

lemma polygonal_middles (hr : 0<r)
    (hsep : ∀ w z, z ∈ D.forbidden w → 5*r<dist (D.point w) z) :
    ∃ U : ForwardDart G → Set ℂ,
      (∀ d, IsOpen (U d) ∧ Disjoint (U d) (D.middleObstacle T d) ∧
        PolygonallyJoined (U d)
          (D.edge d.val.fst d.val.snd d.val.adj (T d).first)
          (D.edge d.val.fst d.val.snd d.val.adj (T d).last)) ∧
      Pairwise (fun d e => Disjoint (U d) (U e)) := by
…

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