Documentation

Mathlib.Analysis.Convex.SpecificFunctions.Basic

Collection of convex functions #

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

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.

TODO #

For p : ℝ, prove that fun x ↦ x ^ p is concave when 0 ≤ p ≤ 1 and strictly concave when 0 < p < 1.

See also #

Analysis.Convex.Mul for convexity of `x ↦ x ^ n``

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

We give an elementary proof rather than using the second derivative test, since this lemma is needed early in the analysis library.

theorem convexOn_exp :

Real.exp is convex on the whole real line.

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 strictConvexOn_rpow {p : } (hp : 1 < p) :
StrictConvexOn (Set.Ici 0) fun (x : ) => x ^ p
theorem convexOn_rpow {p : } (hp : 1 p) :
ConvexOn (Set.Ici 0) fun (x : ) => x ^ p
theorem Real.exp_mul_le_cosh_add_mul_sinh {t : } (ht : |t| 1) (x : ) :