Statement.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PlanarL1.IsPlanar line 11
Source documentation
A topological drawing of a simple graph in the real plane. Each edge is a simple arc, with no vertex in its interior; interiors of distinct unoriented edges are disjoint. Either orientation is available for each edge.
Also declared: ComparatorChallenges/PlanarL1.lean:9 (same declaration text).
```
def IsPlanar {V : Type} (G : SimpleGraph V) : Prop :=
…
```

def OAI.PlanarL1.walkLength line 24

Source documentation

The ordinary sum of edge lengths of a finite graph walk.

Also declared: ComparatorChallenges/PlanarL1.lean:22 (same declaration text).

def walkLength {V : Type} {G : SimpleGraph V} (length : V → V → ℝ)
    {u v : V} : G.Walk u v → ℝ
  | .nil => 0
  | @SimpleGraph.Walk.cons _ _ u w _ _ p => length u w + walkLength length p

/-- Weighted shortest-path distance, as in the first paragraph of the paper.
The main statement requires connectivity and strict positivity on every edge. -/

def OAI.PlanarL1.graphDistance line 31
Source documentation
Weighted shortest-path distance, as in the first paragraph of the paper. The main statement requires connectivity and strict positivity on every edge.
Also declared: ComparatorChallenges/PlanarL1.lean:28 (same declaration text).
```
noncomputable def graphDistance {V : Type} (G : SimpleGraph V)
    (length : V → V → ℝ) (u v : V) : ℝ :=
…
```
def OAI.PlanarL1.MainStatement line 38
Source documentation
Literal universal-distortion target. A graph is indexed by Fin n only to express finite vertex sets without an extraneous universe for the target space. No bound depending on n, edge lengths, or number of scales is permitted.
Also declared: ComparatorChallenges/PlanarL1.lean:34 (same declaration text).
```
def MainStatement : Prop :=
…
```