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
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 α} :