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 : } (hn : even n) :
convex_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 α} (h0 : even (finset.filter (λ (x : α), f x 0) s).card) :
0 ∏ (x : α) in s, f x
theorem int_prod_range_nonneg (m : ) (n : ) (hn : even n) :
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)