Collection of convex functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

strict_convex_on_exp : The exponential function is strictly convex.
even.convex_on_pow: For an even n : ℕ, λ x, x ^ n is convex.
convex_on_pow: For n : ℕ, λ x, x ^ n is convex on $[0, +∞)$.
convex_on_zpow: For m : ℤ, λ x, x ^ m is convex on $[0, +∞)$.
strict_concave_on_log_Ioi, strict_concave_on_log_Iio: real.log is strictly concave on $(0, +∞)$ and $(-∞, 0)$ respectively.
convex_on_rpow, strict_convex_on_rpow : For p : ℝ, λ 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.

TODO #

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

source

theorem strict_convex_on_exp :

strict_convex_on ℝ set.univ rexp

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.

source

theorem convex_on_exp :

convex_on ℝ set.univ rexp

exp is convex on the whole real line.

source

theorem convex_on_pow (n : ℕ) :

convex_on ℝ (set.Ici 0) (λ (x : ℝ), x ^ n)

x^n, n : ℕ is convex on [0, +∞) for all n.

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

source

theorem even.convex_on_pow {n : ℕ} (hn : even n) :

convex_on ℝ set.univ (λ (x : ℝ), x ^ n)

x^n, n : ℕ is convex on the whole real line whenever n is even.

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

source

theorem convex_on_zpow (m : ℤ) :

convex_on ℝ (set.Ioi 0) (λ (x : ℝ), x ^ m)

x^m, m : ℤ is convex on (0, +∞) for all m.

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

source

theorem strict_concave_on_log_Ioi :

strict_concave_on ℝ (set.Ioi 0) real.log

source

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.

source

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.

source

theorem strict_convex_on_rpow {p : ℝ} (hp : 1 < p) :

strict_convex_on ℝ (set.Ici 0) (λ (x : ℝ), x ^ p)

source

theorem convex_on_rpow {p : ℝ} (hp : 1 ≤ p) :

convex_on ℝ (set.Ici 0) (λ (x : ℝ), x ^ p)

source

theorem strict_concave_on_log_Iio :

strict_concave_on ℝ (set.Iio 0) real.log