Collection of convex functions #

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

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

TODO #

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

theorem strict_convex_on_exp :

exp is strictly convex on the whole real line.

theorem convex_on_exp :

exp is convex on the whole real line.

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

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

theorem even.strict_convex_on_pow {n : ℕ} (hn : even n) (h : n ≠ 0) :

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

theorem convex_on_pow (n : ℕ) :

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

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

theorem strict_convex_on_pow {n : ℕ} (hn : 2 ≤ n) :

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

theorem finset.prod_nonneg_of_card_nonpos_even {α : Type u_1} {β : Type u_2} [linear_ordered_comm_ring β] {f : α → β} [decidable_pred (λ (x : α), f x ≤ 0)] {s : finset α} (h0 : even (finset.filter (λ (x : α), f x ≤ 0) s).card) :

0 ≤ s.prod (λ (x : α), f x)