The chord of the real exponential

By convexity, the real exponential lies below its chord over an interval.

Main statements

• Real.exp_mul_le_add_mul: for x ∈ [a, b] with a < b, exp (t * x) is at most the value at x of the chord of s ↦ exp (t * s) through the points a and b.

theorem Real.exp_mul_le_add_mul {a b x : ℝ} (hab : a < b) (hx : x ∈ Set.Icc a b) (t : ℝ) : exp (t * x) ≤ (b * exp (t * a) - a * exp (t * b)) / (b - a) + (exp (t * b) - exp (t * a)) / (b - a) * x

The chord of the exponential lies above it on [a, b].