The scalar estimates behind Birkhoff's contraction theorem

This file collects the scalar inequalities behind Birkhoff's contraction theorem for Hilbert's projective metric (Matrix.hilbertProjectiveDist_mulVec_le in TauCeti/Data/Matrix/BirkhoffContraction.lean). They contain no matrices.

For l ≥ 1, the function σ ↦ log ((1 + l * exp σ) / (l + exp σ)) vanishes at σ = 0 and has derivative l * exp σ / (1 + l * exp σ) - exp σ / (l + exp σ), which is at most (l - 1) / (l + 1) (with equality at σ = 0). It is therefore bounded by (l - 1) / (l + 1) * σ for σ ≥ 0. Writing l = exp (Δ / 2), the slope is tanh (Δ / 4).

Combined with a polynomial inequality, this gives the following for R ≥ 1, l ≥ 1 and positive α, β, α', β'. The logarithmic cross ratio of the pairs (R * α + β, α + β) and (R * α' + β', α' + β') is at most (l - 1) / (l + 1) * log R whenever the pairs (α, β) and (α', β') themselves have cross ratio α * β' / (β * α') at most l ^ 2. This is Birkhoff's theorem in two dimensions.

Main results

• TauCeti.log_one_add_mul_exp_div_add_exp_le: log ((1 + l * exp σ) / (l + exp σ)) ≤ (l - 1) / (l + 1) * σ for 1 ≤ l and 0 ≤ σ.
• TauCeti.birkhoff_cross_ratio_le: the polynomial cross-ratio bound by ((1 + l * s) / (l + s)) ^ 2 for 1 ≤ s and 1 ≤ l.
• TauCeti.log_birkhoff_cross_ratio_le: the two-dimensional form of Birkhoff's theorem, for 1 ≤ R and 1 ≤ l.

References

• G. Birkhoff, Extensions of Jentzsch's theorem, Trans. Amer. Math. Soc. 85 (1957), 219--227.
• E. Seneta, Non-negative Matrices and Markov Chains, Springer (2006), Chapter 3.

theorem TauCeti.log_one_add_mul_exp_div_add_exp_le {l σ : ℝ} (hl : 1 ≤ l) (hσ : 0 ≤ σ) : Real.log ((1 + l * Real.exp σ) / (l + Real.exp σ)) ≤ (l - 1) / (l + 1) * σ

For 1 ≤ l and 0 ≤ σ, log ((1 + l * exp σ) / (l + exp σ)) ≤ (l - 1) / (l + 1) * σ. Both sides vanish at σ = 0, and the derivative of the left side is at most (l - 1) / (l + 1).

theorem TauCeti.birkhoff_cross_ratio_le {α β α' β' s l : ℝ} (hα : 0 < α) (hβ : 0 < β) (hα' : 0 < α') (hβ' : 0 < β') (hs : 1 ≤ s) (hl : 1 ≤ l) (h : α * β' ≤ l ^ 2 * (β * α')) : (s ^ 2 * α + β) * (α' + β') * (l + s) ^ 2 ≤ (1 + l * s) ^ 2 * ((α + β) * (s ^ 2 * α' + β'))

The two-dimensional polynomial inequality behind Birkhoff's theorem. Let 1 ≤ s and 1 ≤ l, and let α, β, α', β' be positive with α * β' ≤ l ^ 2 * (β * α'). Then the cross ratio of (s ^ 2 * α + β, α + β) and (s ^ 2 * α' + β', α' + β') is at most ((1 + l * s) / (l + s)) ^ 2.

theorem TauCeti.log_birkhoff_cross_ratio_le {α β α' β' R l : ℝ} (hα : 0 < α) (hβ : 0 < β) (hα' : 0 < α') (hβ' : 0 < β') (hR : 1 ≤ R) (hl : 1 ≤ l) (h : α * β' ≤ l ^ 2 * (β * α')) : Real.log ((R * α + β) * (α' + β') / ((α + β) * (R * α' + β'))) ≤ (l - 1) / (l + 1) * Real.log R

The two-dimensional form of Birkhoff's theorem: for R ≥ 1, l ≥ 1 and positive α, β, α', β' with α * β' ≤ l ^ 2 * (β * α'), the logarithmic cross ratio of (R * α + β, α + β) and (R * α' + β', α' + β') is at most (l - 1) / (l + 1) * log R.