WeightedMetric.lean`

55 declarations, 0 contain sorry, 0 declared as axioms

Shortest-path spanning tree .

lemma OAI.PlanarL1.WeightedGraph.length_nonneg line 11
lemma OAI.PlanarL1.WeightedGraph.length_pos line 17
lemma OAI.PlanarL1.WeightedGraph.length_append line 23
lemma OAI.PlanarL1.WeightedGraph.length_darts line 29
lemma OAI.PlanarL1.WeightedGraph.length_reverse line 35
lemma OAI.PlanarL1.WeightedGraph.length_bypass_le line 43
lemma OAI.PlanarL1.WeightedGraph.distance_nonneg line 51
lemma OAI.PlanarL1.WeightedGraph.distance_le_length line 57
lemma OAI.PlanarL1.WeightedGraph.distance_self line 63
lemma OAI.PlanarL1.WeightedGraph.distance_attained line 68
lemma OAI.PlanarL1.WeightedGraph.distance_symm line 82
lemma OAI.PlanarL1.WeightedGraph.distance_triangle line 92
lemma OAI.PlanarL1.WeightedGraph.distance_pos line 100
def OAI.PlanarL1.WeightedGraph.metricSpace line 108
lemma OAI.PlanarL1.WeightedGraph.edge_bound line 120

lemma OAI.PlanarL1.WeightedGraph.predecessor line 126

Source documentation

The literal predecessor used in the realization proof can be chosen with strictly decreasing weighted root distance; no unit-edge shortcut is used.

lemma predecessor [Finite V] (hG : G.Connected) (hs : ∀ u v, ℓ u v = ℓ v u)
    (hℓ : ∀ u v, G.Adj u v → 0 < ℓ u v) (o v : V) (hne : v ≠ o) :
    ∃ u, G.Adj u v ∧ graphDistance G ℓ o u+ℓ u v = graphDistance G ℓ o v ∧
      graphDistance G ℓ o u < graphDistance G ℓ o v := by
…

Mentions: OAI.PlanarL1.graphDistance

def OAI.PlanarL1.WeightedGraph.parentGraph line 150
lemma OAI.PlanarL1.WeightedGraph.parent_adj line 158
lemma OAI.PlanarL1.WeightedGraph.parent_connected line 161
lemma OAI.PlanarL1.WeightedGraph.parent_tree line 179
lemma OAI.PlanarL1.WeightedGraph.parent_walk line 213

lemma OAI.PlanarL1.WeightedGraph.shortest_path_tree line 241

Source documentation

The weighted shortest-path spanning tree claimed at . Its tree edges retain their arbitrary original positive lengths.

lemma shortest_path_tree [Finite V] (hG : G.Connected)
    (hs : ∀ u v, ℓ u v = ℓ v u)
    (hℓ : ∀ u v, G.Adj u v → 0 < ℓ u v) (o : V) :
    ∃ T : SimpleGraph V, T ≤ G ∧ T.IsTree ∧
      (∀ v, ∃ p : T.Walk o v, walkLength ℓ p = graphDistance G ℓ o v) ∧
      (∀ u v, T.Adj u v → |graphDistance G ℓ o v-graphDistance G ℓ o u| = ℓ u v) := by
…

Mentions: OAI.PlanarL1.walkLength, OAI.PlanarL1.graphDistance

lemma OAI.PlanarL1.Weighted.length_eq_sum_darts line 284
lemma OAI.PlanarL1.Weighted.length_nonneg line 290
lemma OAI.PlanarL1.Weighted.length_append line 296
lemma OAI.PlanarL1.Weighted.length_reverse line 300
lemma OAI.PlanarL1.Weighted.length_bypass line 307
lemma OAI.PlanarL1.Weighted.length_eq_zero_iff line 315
lemma OAI.PlanarL1.Weighted.exists_shortest line 328
Source documentation
Positivity permits deletion of repetitions, so the literal walk-infimum is achieved by one of finitely many simple paths. No integral edge lengths or approximation of the metric is used.
```
lemma exists_shortest [Fintype V] (hl : ∀ u v, G.Adj u v → 0 ≤ l u v)
    {u v : V} (hc : G.Reachable u v) :
    ∃ p : G.Path u v, ∀ q : G.Walk u v, walkLength l p.val ≤ walkLength l q := by
…
```
Mentions: OAI.PlanarL1.walkLength
lemma OAI.PlanarL1.Weighted.distance_eq_length line 338
lemma OAI.PlanarL1.Weighted.distance_le_walk line 348
lemma OAI.PlanarL1.Weighted.distance_nonneg line 352
lemma OAI.PlanarL1.Weighted.distance_self line 357
lemma OAI.PlanarL1.Weighted.distance_symm line 361
lemma OAI.PlanarL1.Weighted.distance_triangle line 370
lemma OAI.PlanarL1.Weighted.distance_eq_zero line 378

def OAI.PlanarL1.Weighted.metricSpace line 389

Source documentation

The exact source graph metric, on the original vertex type.

@[instance_reducible] noncomputable def metricSpace [Fintype V] (hc : G.Connected)
    (hs : ∀ u v, l u v=l v u) (hl : ∀ u v, G.Adj u v → 0 < l u v) : MetricSpace V where
…

lemma OAI.PlanarL1.Weighted.edge_bound line 398
lemma OAI.PlanarL1.Weighted.height_edge line 402
lemma OAI.PlanarL1.Weighted.exists_predecessor line 417
Source documentation
Each non-root vertex has a strictly lower predecessor on a genuine weighted shortest path. This is the input to the shortest-path spanning tree in ; positivity, not integral weights, supplies the descent.
```
lemma exists_predecessor [Fintype V] (hc : G.Connected)
    (hs : ∀ u v, l u v=l v u) (hl : ∀ u v, G.Adj u v → 0 < l u v)
    (o v : V) (hv : v ≠ o) : ∃ u, G.Adj u v ∧
      graphDistance G l o v=graphDistance G l o u+l u v ∧
      graphDistance G l o u < graphDistance G l o v := by
…
```
Mentions: OAI.PlanarL1.graphDistance
structure OAI.PlanarL1.Weighted.DescendingParents line 459
Source documentation
A predecessor system whose heights strictly decrease to its root. The well-foundedness here uses finiteness, not any discretization of real lengths.
```
structure DescendingParents (V : Type*) where
…
```
lemma OAI.PlanarL1.Weighted.DescendingParents.parent_ne line 470
def OAI.PlanarL1.Weighted.DescendingParents.graph line 476
lemma OAI.PlanarL1.Weighted.DescendingParents.child_adj line 484
lemma OAI.PlanarL1.Weighted.DescendingParents.wellFounded line 487
lemma OAI.PlanarL1.Weighted.DescendingParents.reachable_root line 492
lemma OAI.PlanarL1.Weighted.DescendingParents.connected line 499
lemma OAI.PlanarL1.Weighted.DescendingParents.edge_injective line 504
lemma OAI.PlanarL1.Weighted.DescendingParents.edgeFinset_eq line 516
lemma OAI.PlanarL1.Weighted.DescendingParents.isTree line 532
def OAI.PlanarL1.Weighted.shortestParents line 543
lemma OAI.PlanarL1.Weighted.shortestParents.parent_step line 557
lemma OAI.PlanarL1.Weighted.shortestParents.graph_le line 566
lemma OAI.PlanarL1.Weighted.shortestParents.exists_root_walk line 572
lemma OAI.PlanarL1.Weighted.shortestParents.root_distance line 588
Source documentation
The shortest-path spanning tree in : every root path has the original weighted distance. No planarity or unit edge lengths is used.
```
lemma root_distance (v : V) :
    graphDistance (shortestParents hc hs hl o).graph l o v=graphDistance G l o v := by
…
```
Mentions: OAI.PlanarL1.graphDistance, OAI.PlanarL1.Weighted.shortestParents