Theorem Jlog_strictConvexOn
Jlog : ℝ → ℝ is strictly convex on the entire real line.
Derivation in standard notation:
Jlog(t) ≔ (exp(t) + exp(−t))/2 − 1.
By the identity Jlog_eq_cosh_sub_one, this equals cosh(t) − 1.
The function cosh is strictly convex on ℝ: its second derivative equals cosh itself, which is positive for all real arguments. This is established by cosh_strictly_convex via the criterion strictConvexOn_of_deriv2_pos on the convex set ℝ (univ), using continuity of cosh and the positivity of its second derivative.
StrictConvexOn_cosh is the same statement.
Subtracting the constant −1 preserves strict convexity. The proof of Jlog_strictConvexOn therefore rewrites Jlog pointwise as cosh − 1 and applies the add_const operation to the strict convexity of cosh.
This convexity of Jlog (equivalently of Jcost via the exponential change of variables) is used to obtain the uniqueness result T5 for the cost functional.