OAI.PlanarL1.planar_graph_metrics_embed_L1

The theorem states that the defined proposition MainStatement holds. That proposition asserts there is a real constant C ≥ 1 such that, for every n and every simple graph G on the vertex set {0,…,n−1} that is connected and planar, and every real edge-length function length(u,v) that is symmetric and strictly positive on adjacent pairs, there exist a measurable space Ω, a measure μ on it, and an assignment of each vertex x to an element f(x) of the real L¹(Ω, μ) space, such that for all vertices x and y the L¹ distance ‖f(x) − f(y)‖ is at least graphDistance(x,y) and at most C times graphDistance(x,y). Here graphDistance is the infimum, over all graph walks from x to y, of the walk length, namely the sum of length(u,w) over the walk's consecutive edges. Planar means G has a drawing in the plane ℝ² with distinct vertices at distinct points, one continuous injective arc from the unit interval for each adjacency running from one endpoint to the other, no vertex lying in the interior of any arc, and interior points of arcs coinciding only when the arcs belong to the same unoriented edge. The distortion constant C does not depend on n, G or the lengths, and the embedding is allowed to depend on all of them.