Positive divided differences of the real exponential

The divided difference of the exponential is the integral of the exponential along the segment between its arguments. In particular it is strictly positive, including when the arguments coincide. These are the scalar coefficients in the derivative of the matrix exponential at a Hermitian matrix.

theorem Real.dslope_exp_eq_integral (a b : ℝ) : dslope exp a b = ∫ (t : ℝ) in 0..1, exp ((1 - t) * a + t * b)

The divided difference of the exponential is its average along a segment.

theorem Real.dslope_exp_pos (a b : ℝ) : 0 < dslope exp a b

All divided differences of the real exponential are strictly positive.