Collection of convex functions

In this file we prove that the following functions are convex or strictly convex:

• strictConvexOn_exp : The exponential function is strictly convex.
• strictConcaveOn_log_Ioi, strictConcaveOn_log_Iio: Real.log is strictly concave on $(0, +∞)$ and $(-∞, 0)$ respectively.
• convexOn_rpow, strictConvexOn_rpow : For p : ℝ, fun x ↦ x ^ p is convex on $[0, +∞)$ when 1 ≤ p and strictly convex when 1 < p.

The proofs in this file are deliberately elementary, not by appealing to the sign of the second derivative. This is in order to keep this file early in the import hierarchy, since it is on the path to Hölder's and Minkowski's inequalities and after that to Lp spaces and most of measure theory.

(Strict) concavity of fun x ↦ x ^ p for 0 < p < 1 (0 ≤ p ≤ 1) can be found in Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean.

See also

Mathlib/Analysis/Convex/Mul.lean for convexity of x ↦ x ^ n

theorem strictConvexOn_exp : StrictConvexOn ℝ Set.univ Real.exp

Real.exp is strictly convex on the whole real line.

theorem convexOn_exp : ConvexOn ℝ Set.univ Real.exp

Real.exp is convex on the whole real line.

theorem strictConcaveOn_log_Ioi : StrictConcaveOn ℝ (Set.Ioi 0) Real.log

Real.log is strictly concave on (0, +∞).

theorem one_add_mul_self_lt_rpow_one_add {s : ℝ} (hs : -1 ≤ s) (hs' : s ≠ 0) {p : ℝ} (hp : 1 < p) : 1 + p * s < (1 + s) ^ p

Bernoulli's inequality for real exponents, strict version: for 1 < p and -1 ≤ s, with s ≠ 0, we have 1 + p * s < (1 + s) ^ p.

theorem one_add_mul_self_le_rpow_one_add {s : ℝ} (hs : -1 ≤ s) {p : ℝ} (hp : 1 ≤ p) : 1 + p * s ≤ (1 + s) ^ p

Bernoulli's inequality for real exponents, non-strict version: for 1 ≤ p and -1 ≤ s we have 1 + p * s ≤ (1 + s) ^ p.

theorem rpow_one_add_lt_one_add_mul_self {s : ℝ} (hs : -1 ≤ s) (hs' : s ≠ 0) {p : ℝ} (hp1 : 0 < p) (hp2 : p < 1) : (1 + s) ^ p < 1 + p * s

Bernoulli's inequality for real exponents, strict version: for 0 < p < 1 and -1 ≤ s, with s ≠ 0, we have (1 + s) ^ p < 1 + p * s.

theorem rpow_one_add_le_one_add_mul_self {s : ℝ} (hs : -1 ≤ s) {p : ℝ} (hp1 : 0 ≤ p) (hp2 : p ≤ 1) : (1 + s) ^ p ≤ 1 + p * s

Bernoulli's inequality for real exponents, non-strict version: for 0 ≤ p ≤ 1 and -1 ≤ s we have (1 + s) ^ p ≤ 1 + p * s.

theorem strictConvexOn_rpow {p : ℝ} (hp : 1 < p) : StrictConvexOn ℝ (Set.Ici 0) fun (x : ℝ) => x ^ p

For p : ℝ with 1 < p, fun x ↦ x ^ p is strictly convex on $[0, +∞)$.

theorem convexOn_rpow {p : ℝ} (hp : 1 ≤ p) : ConvexOn ℝ (Set.Ici 0) fun (x : ℝ) => x ^ p

theorem strictConcaveOn_log_Iio : StrictConcaveOn ℝ (Set.Iio 0) Real.log

theorem Real.exp_mul_le_cosh_add_mul_sinh {t : ℝ} (ht : |t| ≤ 1) (x : ℝ) : exp (t * x) ≤ cosh x + t * sinh x