Real trees

A metric space is a real tree if any two points s, t are joined by a geodesic segment, this segment is unique, and every injective continuous path from s to t has the same image as the segment. This is the standard definition.

We prove that a complete metric space satisfying the four-point condition (0-hyperbolicity) and having midpoints is a real tree:

• midpoints and completeness give geodesic segments (dyadic construction);
• the four-point condition forces their uniqueness, and characterizes their points as those c with d(s,c) + d(c,t) = d(s,t);
• removing an interior point of the segment separates s from t (via the Gromov product at that point), so every path from s to t passes through every point of the segment, and injectivity forbids any other point.

The Gromov product and its nonnegativity are reused from Mathlib.

Adapted from Freezing2/Geometry/RealTree.lean in igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit 8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).

def BGW.ContinuumTrees.RealTree.IsSegment {X : Type u_1} [MetricSpace X] (s t : X) (γ : ℝ → X) : Prop

γ parametrizes a geodesic segment from s to t on [0, d(s, t)].

Equations

• BGW.ContinuumTrees.RealTree.IsSegment s t γ = (γ 0 = s ∧ γ (dist s t) = t ∧ ∀ a ∈ Set.Icc 0 (dist s t), ∀ b ∈ Set.Icc 0 (dist s t), dist (γ a) (γ b) = |a - b|)

def BGW.ContinuumTrees.RealTree.IsRealTree (X : Type u_2) [MetricSpace X] : Prop

Real tree. Any two points are joined by a unique geodesic segment, and every injective continuous path between them has the image of that segment.

Equations

• One or more equations did not get rendered due to their size.

def BGW.ContinuumTrees.RealTree.FourPoint (X : Type u_2) [MetricSpace X] : Prop

The four-point condition (0-hyperbolicity).

Equations

• BGW.ContinuumTrees.RealTree.FourPoint X = ∀ (x y z w : X), dist x y + dist z w ≤ max (dist x z + dist y w) (dist x w + dist y z)

def BGW.ContinuumTrees.RealTree.HasMidpoints (X : Type u_2) [MetricSpace X] : Prop

Every pair of points has a midpoint.

Equations

• BGW.ContinuumTrees.RealTree.HasMidpoints X = ∀ (x y : X), ∃ (m : X), dist x m = dist x y / 2 ∧ dist m y = dist x y / 2

def BGW.ContinuumTrees.RealTree.ApproxMidpoints (ε : ℝ) (X : Type u_2) [MetricSpace X] : Prop

Every pair of points has an ε-approximate midpoint.

Equations

• BGW.ContinuumTrees.RealTree.ApproxMidpoints ε X = ∀ (x y : X), ∃ (m : X), |dist x m - dist x y / 2| ≤ ε ∧ |dist m y - dist x y / 2| ≤ ε

theorem BGW.ContinuumTrees.RealTree.IsSegment.dist_left {X : Type u_1} [MetricSpace X] {s t : X} {γ : ℝ → X} (hγ : IsSegment s t γ) {a : ℝ} (ha : a ∈ Set.Icc 0 (dist s t)) : dist s (γ a) = a

theorem BGW.ContinuumTrees.RealTree.IsSegment.dist_right {X : Type u_1} [MetricSpace X] {s t : X} {γ : ℝ → X} (hγ : IsSegment s t γ) {a : ℝ} (ha : a ∈ Set.Icc 0 (dist s t)) : dist (γ a) t = dist s t - a

theorem BGW.ContinuumTrees.RealTree.eq_of_dist_add_dist {X : Type u_1} [MetricSpace X] {s t : X} {γ : ℝ → X} (h4 : FourPoint X) (hγ : IsSegment s t γ) {c : X} (hc : dist s c + dist c t = dist s t) : γ (dist s c) = c

Under the four-point condition a point between s and t lies on every segment.

theorem BGW.ContinuumTrees.RealTree.segment_unique {X : Type u_1} [MetricSpace X] {s t : X} (h4 : FourPoint X) {γ γ' : ℝ → X} (hγ : IsSegment s t γ) (hγ' : IsSegment s t γ') : Set.EqOn γ γ' (Set.Icc 0 (dist s t))

Uniqueness of segments.

theorem BGW.ContinuumTrees.RealTree.continuous_gromovProduct {X : Type u_1} [MetricSpace X] (w x : X) : Continuous (Metric.gromovProduct w x)

theorem BGW.ContinuumTrees.RealTree.gromovProduct_ge_min {X : Type u_1} [MetricSpace X] (h4 : FourPoint X) (w x y z : X) : min (Metric.gromovProduct w x z) (Metric.gromovProduct w z y) ≤ Metric.gromovProduct w x y

theorem BGW.ContinuumTrees.RealTree.isOpen_gromovProduct_eq_zero {X : Type u_1} [MetricSpace X] (h4 : FourPoint X) (c s : X) : IsOpen {p : X | p ≠ c ∧ Metric.gromovProduct c s p = 0}

Points p ≠ c with vanishing Gromov product with s at c form an open set.

theorem BGW.ContinuumTrees.RealTree.mem_image_of_isSegment {X : Type u_1} [MetricSpace X] (h4 : FourPoint X) {s t : X} {γ : ℝ → X} (hγ : IsSegment s t γ) {q : ℝ → X} (hq : ContinuousOn q (Set.Icc 0 1)) (hq0 : q 0 = s) (hq1 : q 1 = t) {a : ℝ} (ha : a ∈ Set.Icc 0 (dist s t)) : γ a ∈ q '' Set.Icc 0 1

Separation. Under the four-point condition, every continuous path from s to t passes through every point of a segment from s to t.

theorem BGW.ContinuumTrees.RealTree.image_eq_of_injOn {X : Type u_1} [MetricSpace X] (h4 : FourPoint X) (hseg : ∀ (x y : X), ∃ (γ : ℝ → X), IsSegment x y γ) {s t : X} {γ : ℝ → X} (hγ : IsSegment s t γ) {q : ℝ → X} (hq : ContinuousOn q (Set.Icc 0 1)) (hinj : Set.InjOn q (Set.Icc 0 1)) (hq0 : q 0 = s) (hq1 : q 1 = t) : q '' Set.Icc 0 1 = γ '' Set.Icc 0 (dist s t)

Arcs are segments. Under the four-point condition, when segments exist between any two points, an injective continuous path from s to t has the image of the segment from s to t.

noncomputable def BGW.ContinuumTrees.RealTree.dyadicSeg {X : Type u_1} (mid : X → X → X) (s t : X) : ℕ → ℕ → X

Dyadic points of a segment built from a midpoint choice.

Equations

• One or more equations did not get rendered due to their size.
• BGW.ContinuumTrees.RealTree.dyadicSeg mid s t 0 x✝ = if x✝ = 0 then s else t

theorem BGW.ContinuumTrees.RealTree.dyadicSeg_zero_right {X : Type u_1} {mid : X → X → X} {s t : X} (m : ℕ) : dyadicSeg mid s t m 0 = s

theorem BGW.ContinuumTrees.RealTree.dyadicSeg_pow {X : Type u_1} {mid : X → X → X} {s t : X} (m : ℕ) : dyadicSeg mid s t m (2 ^ m) = t

theorem BGW.ContinuumTrees.RealTree.dyadicSeg_two_mul {X : Type u_1} {mid : X → X → X} {s t : X} (m i : ℕ) : dyadicSeg mid s t (m + 1) (2 * i) = dyadicSeg mid s t m i

theorem BGW.ContinuumTrees.RealTree.dyadicSeg_adjacent {X : Type u_1} [MetricSpace X] {mid : X → X → X} {s t : X} (hmid : ∀ (x y : X), dist x (mid x y) = dist x y / 2 ∧ dist (mid x y) y = dist x y / 2) (m i : ℕ) : i < 2 ^ m → dist (dyadicSeg mid s t m i) (dyadicSeg mid s t m (i + 1)) = dist s t / 2 ^ m

theorem BGW.ContinuumTrees.RealTree.dyadicSeg_dist_le {X : Type u_1} [MetricSpace X] {mid : X → X → X} {s t : X} (hmid : ∀ (x y : X), dist x (mid x y) = dist x y / 2 ∧ dist (mid x y) y = dist x y / 2) (m : ℕ) {i : ℕ} (j : ℕ) : i ≤ j → j ≤ 2 ^ m → dist (dyadicSeg mid s t m i) (dyadicSeg mid s t m j) ≤ (↑j - ↑i) * (dist s t / 2 ^ m)

theorem BGW.ContinuumTrees.RealTree.dyadicSeg_dist {X : Type u_1} [MetricSpace X] {mid : X → X → X} {s t : X} (hmid : ∀ (x y : X), dist x (mid x y) = dist x y / 2 ∧ dist (mid x y) y = dist x y / 2) (m : ℕ) {i j : ℕ} (hi : i ≤ 2 ^ m) (hj : j ≤ 2 ^ m) : dist (dyadicSeg mid s t m i) (dyadicSeg mid s t m j) = |↑i - ↑j| * (dist s t / 2 ^ m)

theorem BGW.ContinuumTrees.RealTree.floor_two_mul_bounds {y : ℝ} (hy : 0 ≤ y) : ⌊2 * y⌋₊ = 2 * ⌊y⌋₊ ∨ ⌊2 * y⌋₊ = 2 * ⌊y⌋₊ + 1

theorem BGW.ContinuumTrees.RealTree.exists_isSegment {X : Type u_1} [MetricSpace X] [CompleteSpace X] (hm : HasMidpoints X) (s t : X) : ∃ (γ : ℝ → X), IsSegment s t γ

Segments from midpoints. In a complete metric space with midpoints, any two points are joined by a geodesic segment.

theorem BGW.ContinuumTrees.RealTree.hasMidpoints_of_approx {X : Type u_1} [MetricSpace X] [CompactSpace X] (h : ∀ ε > 0, ApproxMidpoints ε X) : HasMidpoints X

Approximate midpoints at every scale give exact midpoints in a compact space.

theorem BGW.ContinuumTrees.RealTree.isRealTree_of_fourPoint {X : Type u_1} [MetricSpace X] [CompleteSpace X] (h4 : FourPoint X) (hm : HasMidpoints X) : IsRealTree X

Complete 0-hyperbolic spaces with midpoints are real trees.

theorem BGW.ContinuumTrees.RealTree.FourPoint.of_isometryEquiv {X : Type u_1} [MetricSpace X] {Y : Type u_2} [MetricSpace Y] (e : X ≃ᵢ Y) (h : FourPoint X) : FourPoint Y

theorem BGW.ContinuumTrees.RealTree.ApproxMidpoints.of_isometryEquiv {X : Type u_1} [MetricSpace X] {Y : Type u_2} [MetricSpace Y] (e : X ≃ᵢ Y) {ε : ℝ} (h : ApproxMidpoints ε X) : ApproxMidpoints ε Y