Gromov-hyperbolic spaces

DefinitionGromov \(\delta\)-hyperbolic space#✓fully proved

A pseudometric space X is δ-hyperbolic (in the sense of Gromov) if 0 ≤ δ and the Gromov product satisfies the four-point inequality (x ∣ z)_w ≥ min (x ∣ y)_w (y ∣ z)_w - δ for all points w x y z, where (x ∣ y)_w = Metric.gromovProduct w x y (basepoint first, as in Mathlib).

def IsDeltaHyperbolic (X : Type*) [PseudoMetricSpace X] (δ : ℝ) : Prop :=
  0 ≤ δ ∧ ∀ w x y z : X, min (gromovProduct w x y) (gromovProduct w y z) - δ ≤ gromovProduct w x z

Used by 8

Used byFour-point inequality of a \(\delta\)-hyperbolic space · A space with at most one point is \(0\)-hyperbolic · Gromov-hyperbolic spaces · Hyperbolicity is monotone in the constant · The hyperbolicity constant is nonnegative · Word-hyperbolic groups are finitely generated · Word-hyperbolic groups · The trivial group is word-hyperbolic

DefinitionGromov-hyperbolic spaces#✓fully proved

A pseudometric space \(X\) is Gromov-hyperbolic if there is a real number \(\delta\) such that \(X\) is \(\delta\)-hyperbolic.

def IsGromovHyperbolic (X : Type*) [PseudoMetricSpace X] : Prop := ∃ δ : ℝ, IsDeltaHyperbolic X δ

Uses 1

Statement usesGromov \(\delta\)-hyperbolic space

TheoremFour-point inequality of a \(\delta\)-hyperbolic space#✓fully proved

The defining four-point inequality of a δ-hyperbolic space.

theorem IsDeltaHyperbolic.four_point {δ : ℝ} (h : IsDeltaHyperbolic X δ) (w x y z : X) :
    min (gromovProduct w x y) (gromovProduct w y z) - δ ≤ gromovProduct w x z

Uses 1 · Used by 1

Statement usesGromov \(\delta\)-hyperbolic space

Used byHyperbolicity is monotone in the constant

TheoremHyperbolicity is monotone in the constant#✓fully proved

If a pseudometric space \(X\) is \(\delta\)-hyperbolic and \(\delta \le \delta'\), then \(X\) is \(\delta'\)-hyperbolic.

theorem IsDeltaHyperbolic.mono {δ δ' : ℝ} (h : IsDeltaHyperbolic X δ) (hδ : δ ≤ δ') :
    IsDeltaHyperbolic X δ'

Uses 2

Statement usesGromov \(\delta\)-hyperbolic space

Proof usesFour-point inequality of a \(\delta\)-hyperbolic space

TheoremThe hyperbolicity constant is nonnegative#✓fully proved

If a pseudometric space \(X\) is \(\delta\)-hyperbolic, then \(\delta \ge 0\).

theorem IsDeltaHyperbolic.nonneg {δ : ℝ} (h : IsDeltaHyperbolic X δ) : 0 ≤ δ

Uses 1

Statement usesGromov \(\delta\)-hyperbolic space

TheoremA space with at most one point is \(0\)-hyperbolic#✓fully proved

Every pseudometric space \(X\) with at most one point is \(0\)-hyperbolic.

theorem isDeltaHyperbolic_zero_of_subsingleton [Subsingleton X] : IsDeltaHyperbolic X 0

Uses 1

Statement usesGromov \(\delta\)-hyperbolic space

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.