Embedding.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.PlanarL1.Columns.Model.Ambient.exists_uniform_cuts line 19
Source documentation
The actual finite coupled process produces a cut metric with a universal lower bound. The finite initial units, mesh and number of steps are selected from the given vertices; they do not enter the distortion constant.
```
lemma exists_uniform_cuts : ∃ C : FiniteL1.CutFamily V, ∀ x y,
    (scheduleGain/(q:ℝ))*dist (v x) (v y) ≤ C.distance x y ∧
      C.distance x y ≤ 2*dist (v x) (v y) := by
…
```
Mentions: OAI.PlanarL1.FiniteL1.CutFamily

lemma OAI.PlanarL1.Columns.Model.Ambient.exists_L1_embedding line 61

Source documentation

A finite-dimensional real L1 embedding of vertices of any connected terminal noncrossing column model, with a constant depending only on q.

lemma exists_L1_embedding : ∃ (Ω : Type u) (measurable : MeasurableSpace Ω)
    (μ : @MeasureTheory.Measure Ω measurable)
    (f : V → @MeasureTheory.Lp Ω ℝ measurable _ 1 μ), ∀ x y,
      dist (v x) (v y) ≤ ‖f x-f y‖ ∧
      ‖f x-f y‖ ≤ (2/(scheduleGain/(q:ℝ)))*dist (v x) (v y) := by
…

def OAI.PlanarL1.HeightTree.Layout.ambient line 82
theorem OAI.PlanarL1.planar_graph_metrics_embed_L1 line 96
Source documentation
Theorem 1.1 of the literal source. The spacing is selected once, before any graph or length data. Its finite cut embedding is converted to real Lp1. All geometric realization and process hypotheses are discharged above.
Distinct definitions of this name: ComparatorChallenges/PlanarL1.lean:46 (same statement text; different proof or body). Qualify references as OAI.PlanarL1.planar_graph_metrics_embed_L1@path.
```
theorem planar_graph_metrics_embed_L1 : MainStatement := by
…
```
Mentions: OAI.PlanarL1.MainStatement