feat: exp (t * x) ≤ cosh x + t * sinh x (#9097)

From LeanAPAP

Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean

@@ -216,3 +216,16 @@ theorem strictConcaveOn_log_Iio : StrictConcaveOn ℝ (Iio 0) log := by
     _ = _ := by rw [log_neg_eq_log]
 
 #align strict_concave_on_log_Iio strictConcaveOn_log_Iio
+
+namespace Real
+
+lemma exp_mul_le_cosh_add_mul_sinh {t : ℝ} (ht : |t| ≤ 1) (x : ℝ) :
+    exp (t * x) ≤ cosh x + t * sinh x := by
+  rw [abs_le] at ht
+  calc
+    _ = exp ((1 + t) / 2 * x + (1 - t) / 2 * (-x)) := by ring_nf
+    _ ≤ (1 + t) / 2 * exp x + (1 - t) / 2 * exp (-x) :=
+        convexOn_exp.2 (Set.mem_univ _) (Set.mem_univ _) (by linarith) (by linarith) $ by ring
+    _ = _ := by rw [cosh_eq, sinh_eq]; ring
+
+end Real