The recession constant of a function on the half-line

The recession constant of U : ℝ → ℝ is the asymptotic slope U'(∞) = lim_{s → ∞} U(s) / s, an extended real. It measures how U grows at infinity, and it is the coefficient that the internal energy ∫ U(ρ) dm of a measure assigns to its part singular with respect to the reference measure m: concentrating mass M on an m-null set costs U'(∞) M.

The constant is defined as an upper limit (TauCeti.recessionConstant), so it exists for every function. For U convex on [0, ∞) the slopes (U s - U 0) / s are monotone, so U(s) / s genuinely converges to it (ConvexOn.tendsto_div_recessionConstant).

Main definitions

• TauCeti.recessionConstant U: the upper limit of U(s) / s as s → ∞, in EReal.

Main results

• ConvexOn.tendsto_div_recessionConstant: for U convex on [0, ∞), U(s) / s tends to the recession constant.
• TauCeti.recessionConstant_mul_log: the recession constant of r ↦ r log r is ⊤.

References

• L. Ambrosio, N. Gigli, G. Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, 2nd ed., Birkhäuser 2008, §9.3.
• C. Villani, Optimal Transport: Old and New, Springer 2009, Chapter 17.

noncomputable def TauCeti.recessionConstant (U : ℝ → ℝ) : EReal

The recession constant U'(∞) = lim_{s → ∞} U(s) / s of a function U : ℝ → ℝ, as an extended real. It is defined as the upper limit of U(s) / s, so it exists for every U; for U convex on [0, ∞) it is a genuine limit (ConvexOn.tendsto_div_recessionConstant).

theorem TauCeti.recessionConstant_def (U : ℝ → ℝ) : recessionConstant U = Filter.limsup (fun (s : ℝ) => ↑(U s / s)) Filter.atTop

The defining formula of the recession constant, as the upper limit of U(s) / s.

theorem TauCeti.recessionConstant_eq_of_tendsto {U : ℝ → ℝ} {L : EReal} (h : Filter.Tendsto (fun (s : ℝ) => ↑(U s / s)) Filter.atTop (nhds L)) : recessionConstant U = L

If U(s) / s tends to L as s → ∞, then L is the recession constant of U.

theorem TauCeti.recessionConstant_mul_log : (recessionConstant fun (r : ℝ) => r * Real.log r) = ⊤

The recession constant of r ↦ r log r is ⊤: its slopes log s are unbounded.

theorem ConvexOn.tendsto_div_recessionConstant {U : ℝ → ℝ} (hU : ConvexOn ℝ (Set.Ici 0) U) : Filter.Tendsto (fun (s : ℝ) => ↑(U s / s)) Filter.atTop (nhds (TauCeti.recessionConstant U))

For U convex on [0, ∞), U(s) / s tends to the recession constant of U as s → ∞.