mathlib documentation

analysis.convex.specific_functions

Collection of convex functions #

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

TODO #

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

exp is strictly convex on the whole real line.

exp is convex on the whole real line.

theorem even.convex_on_pow {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 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) :
strict_convex_on (set.Ici 0) (λ (x : ), x ^ n)

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

theorem real.pow_sum_div_card_le_sum_pow {α : Type u_1} {s : finset α} {f : α → } (n : ) (hf : ∀ (a : α), a s0 f a) :
s.sum (λ (x : α), f x) ^ (n + 1) / (s.card) ^ n s.sum (λ (x : α), f x ^ (n + 1))

Specific case of Jensen's inequality for sums of powers

theorem nnreal.pow_sum_div_card_le_sum_pow {α : Type u_1} (s : finset α) (f : α → nnreal) (n : ) :
s.sum (λ (x : α), f x) ^ (n + 1) / (s.card) ^ n s.sum (λ (x : α), f x ^ (n + 1))
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)
theorem int_prod_range_nonneg (m : ) (n : ) (hn : even n) :
0 (finset.range n).prod (λ (k : ), m - k)
theorem int_prod_range_pos {m : } {n : } (hn : even n) (hm : m set.Ico 0 n) :
0 < (finset.range n).prod (λ (k : ), m - k)
theorem convex_on_zpow (m : ) :
convex_on (set.Ioi 0) (λ (x : ), x ^ m)

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

theorem strict_convex_on_zpow {m : } (hm₀ : m 0) (hm₁ : m 1) :
strict_convex_on (set.Ioi 0) (λ (x : ), x ^ m)

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

theorem convex_on_rpow {p : } (hp : 1 p) :
convex_on (set.Ici 0) (λ (x : ), x ^ p)
theorem strict_convex_on_rpow {p : } (hp : 1 < p) :
strict_convex_on (set.Ici 0) (λ (x : ), x ^ p)
theorem has_deriv_at_sqrt_mul_log {x : } (hx : x 0) :
has_deriv_at (λ (x : ), real.sqrt x * real.log x) ((2 + real.log x) / (2 * real.sqrt x)) x
theorem deriv_sqrt_mul_log (x : ) :
deriv (λ (x : ), real.sqrt x * real.log x) x = (2 + real.log x) / (2 * real.sqrt x)
theorem deriv_sqrt_mul_log'  :
deriv (λ (x : ), real.sqrt x * real.log x) = λ (x : ), (2 + real.log x) / (2 * real.sqrt x)
theorem deriv2_sqrt_mul_log (x : ) :
deriv^[2] (λ (x : ), real.sqrt x * real.log x) x = -real.log x / (4 * real.sqrt x ^ 3)