Hilbert's projective metric and Birkhoff's contraction theorem

For two vectors x y : ι → ℝ over a finite type, Hilbert's projective metric is TauCeti.hilbertProjectiveDist x y = ⨆ i, ⨆ j, log (x i * y j / (y i * x j)). On strictly positive vectors this is the classical log (max_i (x i / y i) / min_i (x i / y i)): it is a pseudometric which vanishes exactly on proportional vectors, so it is a metric on the rays of the positive orthant. It is unchanged by rescaling either argument, by a common diagonal scaling of both arguments, and by taking entrywise inverses.

A matrix K with strictly positive entries maps the positive orthant into itself, and its projective diameter Matrix.projectiveDiameter K is the Hilbert diameter of its columns, Δ(K) = ⨆ i i' j j', log (K i j * K i' j' / (K i j' * K i' j)). Every image K *ᵥ u of a nonnegative vector lies within Δ(K) of every other. Birkhoff's theorem sharpens this to a contraction: K contracts Hilbert's projective metric by the factor tanh (Δ(K) / 4) < 1.

Diagonal scaling invariance, inversion invariance and the contraction of K and of its transpose are what make the alternating row and column normalisations of a positive kernel (the Sinkhorn iteration) a contraction for Hilbert's projective metric.

Main definitions

• TauCeti.hilbertProjectiveDist x y: Hilbert's projective metric between two real vectors.
• Matrix.projectiveDiameter K: Birkhoff's projective diameter of a matrix.

Main results

• TauCeti.hilbertProjectiveDist_triangle, TauCeti.hilbertProjectiveDist_comm and TauCeti.hilbertProjectiveDist_eq_zero_iff: the pseudometric laws, with zero distance exactly for proportional positive vectors.
• TauCeti.hilbertProjectiveDist_smul_left, TauCeti.hilbertProjectiveDist_mul_left and TauCeti.hilbertProjectiveDist_inv: invariance under rescaling, diagonal scaling and inversion.
• Matrix.hilbertProjectiveDist_mulVec_le_projectiveDiameter: the images of nonnegative vectors under a positive matrix lie within its projective diameter of each other.
• Matrix.hilbertProjectiveDist_mulVec_le: Birkhoff's contraction theorem, d (K *ᵥ x) (K *ᵥ y) ≤ tanh (Δ(K) / 4) * d x y for a strictly positive matrix K and strictly positive vectors x and y.

References

• G. Birkhoff, Extensions of Jentzsch's theorem, Trans. Amer. Math. Soc. 85 (1957), 219--227.
• P. J. Bushell, Hilbert's metric and positive contraction mappings in a Banach space, Arch. Rational Mech. Anal. 52 (1973), 330--338.
• E. Seneta, Non-negative Matrices and Markov Chains, Springer (2006), Chapter 3.
• G. Peyré and M. Cuturi, Computational Optimal Transport, Found. Trends Mach. Learn. 11 (2019), Section 4.2, for the use of this contraction in the Sinkhorn iteration.

Hilbert's projective metric

noncomputable def TauCeti.hilbertProjectiveDist {ι : Type u_1} (x y : ι → ℝ) : ℝ

Hilbert's projective metric between two real vectors, the supremum over all pairs of indices of the logarithm of the cross ratio x i * y j / (y i * x j).

For strictly positive x and y this is log (max_i (x i / y i) / min_i (x i / y i)); the pseudometric laws below are stated under the positivity they use. The formula is defined for all real vectors, with Mathlib's conventions a / 0 = 0 and Real.log 0 = 0.

Equations

• TauCeti.hilbertProjectiveDist x y = ⨆ (i : ι), ⨆ (j : ι), Real.log (x i * y j / (y i * x j))

theorem TauCeti.hilbertProjectiveDist_def {ι : Type u_1} (x y : ι → ℝ) : hilbertProjectiveDist x y = ⨆ (i : ι), ⨆ (j : ι), Real.log (x i * y j / (y i * x j))

The defining formula of Hilbert's projective metric.

theorem TauCeti.log_le_hilbertProjectiveDist {ι : Type u_1} [Finite ι] (x y : ι → ℝ) (i j : ι) : Real.log (x i * y j / (y i * x j)) ≤ hilbertProjectiveDist x y

Each logarithmic cross ratio is at most Hilbert's projective metric.

theorem TauCeti.hilbertProjectiveDist_le {ι : Type u_1} {x y : ι → ℝ} {C : ℝ} (h : ∀ (i j : ι), Real.log (x i * y j / (y i * x j)) ≤ C) (hC : 0 ≤ C) : hilbertProjectiveDist x y ≤ C

Hilbert's projective metric is at most any nonnegative bound on all logarithmic cross ratios.

theorem TauCeti.hilbertProjectiveDist_nonneg {ι : Type u_1} [Finite ι] (x y : ι → ℝ) : 0 ≤ hilbertProjectiveDist x y

Hilbert's projective metric is nonnegative: the diagonal cross ratios have logarithm 0.

@[simp]

theorem TauCeti.hilbertProjectiveDist_self {ι : Type u_1} (x : ι → ℝ) : hilbertProjectiveDist x x = 0

Every vector is at Hilbert distance 0 from itself.

theorem TauCeti.hilbertProjectiveDist_comm {ι : Type u_1} [Finite ι] (x y : ι → ℝ) : hilbertProjectiveDist x y = hilbertProjectiveDist y x

Hilbert's projective metric is symmetric.

theorem TauCeti.hilbertProjectiveDist_triangle {ι : Type u_1} [Finite ι] (x z : ι → ℝ) {y : ι → ℝ} (hy : ∀ (i : ι), y i ≠ 0) : hilbertProjectiveDist x z ≤ hilbertProjectiveDist x y + hilbertProjectiveDist y z

The triangle inequality for Hilbert's projective metric. Only the middle vector needs nonzero entries.

@[simp]

theorem TauCeti.hilbertProjectiveDist_smul_left {ι : Type u_1} {c : ℝ} (hc : c ≠ 0) (x y : ι → ℝ) : hilbertProjectiveDist (c • x) y = hilbertProjectiveDist x y

Rescaling the first vector by a nonzero scalar does not change Hilbert's projective metric.

@[simp]

theorem TauCeti.hilbertProjectiveDist_smul_right {ι : Type u_1} {c : ℝ} (hc : c ≠ 0) (x y : ι → ℝ) : hilbertProjectiveDist x (c • y) = hilbertProjectiveDist x y

Rescaling the second vector by a nonzero scalar does not change Hilbert's projective metric.

theorem TauCeti.hilbertProjectiveDist_mul_left {ι : Type u_1} {w : ι → ℝ} (hw : ∀ (i : ι), w i ≠ 0) (x y : ι → ℝ) : hilbertProjectiveDist (w * x) (w * y) = hilbertProjectiveDist x y

A common diagonal scaling by a vector with nonzero entries does not change Hilbert's projective metric.

@[simp]

theorem TauCeti.hilbertProjectiveDist_inv {ι : Type u_1} [Finite ι] (x y : ι → ℝ) : hilbertProjectiveDist x⁻¹ y⁻¹ = hilbertProjectiveDist x y

Taking entrywise inverses does not change Hilbert's projective metric.

theorem TauCeti.hilbertProjectiveDist_eq_zero_iff {ι : Type u_1} [Finite ι] {x y : ι → ℝ} (hx : ∀ (i : ι), 0 < x i) (hy : ∀ (i : ι), 0 < y i) : hilbertProjectiveDist x y = 0 ↔ ∃ (c : ℝ), 0 < c ∧ x = c • y

Hilbert's projective metric vanishes on two strictly positive vectors exactly when they are proportional.

Birkhoff's contraction theorem

noncomputable def Matrix.projectiveDiameter {ι : Type u_1} {κ : Type u_2} (K : Matrix ι κ ℝ) : ℝ

Birkhoff's projective diameter of a matrix: the Hilbert projective diameter of its columns, ⨆ j, ⨆ j', hilbertProjectiveDist (fun i ↦ K i j) (fun i ↦ K i j').

For a matrix with strictly positive entries this is the classical Δ(K) = log max_{i, i', j, j'} (K i j * K i' j' / (K i j' * K i' j)), and it bounds the Hilbert distance between any two images of nonnegative vectors under K.

Equations

• K.projectiveDiameter = ⨆ (j : κ), ⨆ (j' : κ), TauCeti.hilbertProjectiveDist (fun (i : ι) => K i j) fun (i : ι) => K i j'

theorem Matrix.projectiveDiameter_def {ι : Type u_1} {κ : Type u_2} (K : Matrix ι κ ℝ) : K.projectiveDiameter = ⨆ (j : κ), ⨆ (j' : κ), TauCeti.hilbertProjectiveDist (fun (i : ι) => K i j) fun (i : ι) => K i j'

The defining formula of the projective diameter.

theorem Matrix.log_le_projectiveDiameter {ι : Type u_1} {κ : Type u_2} [Finite ι] [Finite κ] (K : Matrix ι κ ℝ) (i i' : ι) (j j' : κ) : Real.log (K i j * K i' j' / (K i j' * K i' j)) ≤ K.projectiveDiameter

Each logarithmic cross ratio of the entries of K is at most its projective diameter.

theorem Matrix.projectiveDiameter_nonneg {ι : Type u_1} {κ : Type u_2} [Finite ι] (K : Matrix ι κ ℝ) : 0 ≤ K.projectiveDiameter

The projective diameter of a matrix is nonnegative.

theorem Matrix.projectiveDiameter_le {ι : Type u_1} {κ : Type u_2} {K : Matrix ι κ ℝ} {C : ℝ} (h : ∀ (i i' : ι) (j j' : κ), Real.log (K i j * K i' j' / (K i j' * K i' j)) ≤ C) (hC : 0 ≤ C) : K.projectiveDiameter ≤ C

The projective diameter of a matrix is at most any nonnegative bound on all logarithmic cross ratios of its entries.

@[simp]

theorem Matrix.projectiveDiameter_transpose {ι : Type u_1} {κ : Type u_2} [Finite ι] [Finite κ] (K : Matrix ι κ ℝ) : K.transpose.projectiveDiameter = K.projectiveDiameter

A matrix and its transpose have the same projective diameter: both are the supremum of the same logarithmic cross ratios of entries.

theorem Matrix.hilbertProjectiveDist_mulVec_le_projectiveDiameter {ι : Type u_1} {κ : Type u_2} [Finite ι] [Fintype κ] {K : Matrix ι κ ℝ} (hK : ∀ (i : ι) (j : κ), 0 < K i j) {u v : κ → ℝ} (hu : ∀ (j : κ), 0 ≤ u j) (hv : ∀ (j : κ), 0 ≤ v j) : TauCeti.hilbertProjectiveDist (K.mulVec u) (K.mulVec v) ≤ K.projectiveDiameter

The images of two nonnegative vectors under a matrix with strictly positive entries lie within its projective diameter of each other.

theorem Matrix.hilbertProjectiveDist_mulVec_le {ι : Type u_1} {κ : Type u_2} [Finite ι] [Fintype κ] {K : Matrix ι κ ℝ} (hK : ∀ (i : ι) (j : κ), 0 < K i j) {x y : κ → ℝ} (hx : ∀ (j : κ), 0 < x j) (hy : ∀ (j : κ), 0 < y j) : TauCeti.hilbertProjectiveDist (K.mulVec x) (K.mulVec y) ≤ Real.tanh (K.projectiveDiameter / 4) * TauCeti.hilbertProjectiveDist x y

Birkhoff's contraction theorem. A matrix K with strictly positive entries contracts Hilbert's projective metric between strictly positive vectors by the factor tanh (K.projectiveDiameter / 4), which is strictly less than 1.