Collection of convex functions

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

convex_on_exp : the exponential function is convex on $(-∞, +∞)$;
convex_on_pow_of_even : given an even natural number $n$, the function $f(x)=x^n$ is convex on $(-∞, +∞)$;
convex_on_pow : for a natural $n$, the function $f(x)=x^n$ is convex on $[0, +∞)$;
convex_on_fpow : for an integer $m$, the function $f(x)=x^m$ is convex on $(0, +∞)$.
convex_on_rpow : ∀ p : ℝ, 1 ≤ p → convex_on (Ici 0) (λ x, x ^ p)

theorem convex_on_exp :

exp is convex on the whole real line

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

x^n, n : ℕ is convex on the whole real line whenever n 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 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 : (finset.filter (λ (x : α), f x ≤ 0) s).card.even) :

0 ≤ ∏ (x : α) in s, f x

theorem int_prod_range_nonneg (m : ℤ) (n : ℕ) (hn : n.even) :

0 ≤ ∏ (k : ℕ) in finset.range n, (m - ↑k)

theorem convex_on_fpow (m : ℤ) :

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

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

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

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