Documentation

Mathlib.Topology.MetricSpace.GromovProduct

The Gromov product #

The Gromov product of y and z with respect to x in a pseudometric space is (y, z)_x = (dist x y + dist x z - dist y z) / 2.

Main definitions #

Tags #

Gromov product

Implementation notes #

We intentionally omit grind tags which would introduce dist terms in general proofs about gromovProduct, to avoid introducing the dist-theory. In proofs where it is useful to convert gromovProduct to a dist, users should feel free to add the relevant lemmas to the grind [...] list in an application.

source
noncomputable def Metric.gromovProduct {X : Type u_1} [PseudoMetricSpace X] (x y z : X) :
ℝ

The Gromov product of y and z with respect to x.

Equations
Instances For
    source
    theorem Metric.gromovProduct_eq {X : Type u_1} [PseudoMetricSpace X] (x y z : X) :
    gromovProduct x y z = (dist x y + dist x z - dist y z) / 2
    source
    theorem Metric.gromovProduct_comm {X : Type u_1} [PseudoMetricSpace X] (x y z : X) :
    gromovProduct x y z = gromovProduct x z y
    source
    theorem Metric.gromovProduct_nonneg {X : Type u_1} [PseudoMetricSpace X] (x y z : X) :
    0 ≤ gromovProduct x y z
    source
    theorem Metric.gromovProduct_le_dist_left {X : Type u_1} [PseudoMetricSpace X] (x y z : X) :
    gromovProduct x y z ≤ dist x y
    source
    theorem Metric.gromovProduct_le_dist_right {X : Type u_1} [PseudoMetricSpace X] (x y z : X) :
    gromovProduct x y z ≤ dist x z
    source
    @[simp]
    theorem Metric.gromovProduct_self_left {X : Type u_1} [PseudoMetricSpace X] (x y : X) :
    gromovProduct x x y = 0
    source
    @[simp]
    theorem Metric.gromovProduct_self_right {X : Type u_1} [PseudoMetricSpace X] (x y : X) :
    gromovProduct x y x = 0
    source
    @[simp]
    theorem Metric.gromovProduct_self {X : Type u_1} [PseudoMetricSpace X] (x y : X) :
    gromovProduct x y y = dist x y
    source
    theorem Metric.gromovProduct_add_gromovProduct₁₃ {X : Type u_1} [PseudoMetricSpace X] (x y z : X) :
    gromovProduct x y z + gromovProduct z y x = dist x z
    source
    theorem Metric.gromovProduct_add_gromovProduct₁₂ {X : Type u_1} [PseudoMetricSpace X] (x y z : X) :
    gromovProduct x y z + gromovProduct y x z = dist x y