mathlib documentation

analysis.convex.specific_functions

Collection of convex functions

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

exp is convex on the whole real line

theorem convex_on_pow_of_even {n : } :
even nconvex_on set.univ (λ (x : ), x ^ n)

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 α} :
even (finset.filter (λ (x : α), f x 0) s).card0 ∏ (x : α) in s, f x

theorem int_prod_range_nonneg (m : ) (n : ) :
even n0 ∏ (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 : } :
1 pconvex_on (set.Ici 0) (λ (x : ), x ^ p)