Distortion.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ForestSpace.Diamond.LensProperty line 21
Source documentation
The exact separated approximate-midpoint estimate proved for the target space.
```
def LensProperty (E : Type) [NormedAddCommGroup E] [NormedSpace ℝ E] : Prop :=
…
```
theorem OAI.ForestSpace.Diamond.parent_step line 26

theorem OAI.ForestSpace.Diamond.edge_sq_loss line 69

Source documentation

The squared loss holds on each original edge, without requiring attainment of any supremum of edge stretches.

 theorem edge_sq_loss (hLens : LensProperty E) (A : Network) (hA : A.graph.Connected)
    (n : ℕ) (f : (A.iterate n).V → E) (C : ℝ) (hC : 0 ≤ C)
    (hl : ∀ u v, ((A.iterate n).graph.dist u v : ℝ) ≤ ‖f u-f v‖)
    (hu : ∀ u v, ‖f u-f v‖ ≤ C*((A.iterate n).graph.dist u v : ℝ))
    (e : A.E) :
    (‖f (A.old n (A.right e))-f (A.old n (A.left e))‖/(2:ℝ)^n)^2+(n:ℝ)/12 ≤ C^2 := by
…

Mentions: OAI.ForestSpace.Diamond.LensProperty, OAI.ForestSpace.Diamond.Network, OAI.ForestSpace.e

def OAI.ForestSpace.Diamond.EmbeddingBound line 139
Source documentation
The distortion convention, including its arbitrary positive scale.
Also declared: ComparatorChallenges/ForestSpace.lean:444 (same declaration text).
```
def EmbeddingBound (k : ℕ) (f : (diamond k).V → E) (C : ℝ) : Prop :=
…
```
Mentions: OAI.ForestSpace.Diamond.diamond
theorem OAI.ForestSpace.Diamond.distortion_lower line 143
theorem OAI.ForestSpace.main_diamond_distortion line 188
Source documentation
The distortion bound, with the positive-scale bi-Lipschitz convention and the actual shortest-path distance on D_k.
```
theorem main_diamond_distortion (k : ℕ)
    (f : (Diamond.diamond k).V → FullDual Vertex) (C : ℝ)
    (hf : Diamond.EmbeddingBound k f C) :
    Real.sqrt (1+(k:ℝ)/12) ≤ C :=
…
```
Mentions: OAI.ForestSpace.Diamond.diamond, OAI.ForestSpace.FullDual, OAI.ForestSpace.Vertex, OAI.ForestSpace.Diamond.EmbeddingBound