# mathlib3documentation

analysis.convex.specific_functions.deriv

# Collection of convex functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove that certain specific functions are strictly convex, including the following:

• even.strict_convex_on_pow : For an even n : ℕ with 2 ≤ n, λ x, x ^ n is strictly convex.
• strict_convex_on_pow : For n : ℕ, with 2 ≤ n, λ x, x ^ n is strictly convex on $[0, +∞)$.
• strict_convex_on_zpow : For m : ℤ with m ≠ 0, 1, λ x, x ^ m is strictly convex on $[0, +∞)$.
• strict_concave_on_sin_Icc : sin is strictly concave on $[0, π]$
• strict_concave_on_cos_Icc : cos is strictly concave on $[-π/2, π/2]$

## TODO #

These convexity lemmas are proved by checking the sign of the second derivative. If desired, most of these could also be switched to elementary proofs, like in analysis.convex.specific_functions.basic.

theorem strict_convex_on_pow {n : } (hn : 2 n) :
(λ (x : ), x ^ n)

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

theorem even.strict_convex_on_pow {n : } (hn : even n) (h : n 0) :
(λ (x : ), x ^ n)

x^n, n : ℕ is strictly convex on the whole real line whenever n ≠ 0 is even.

theorem finset.prod_nonneg_of_card_nonpos_even {α : Type u_1} {β : Type u_2} {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 n) :
0 < (finset.range n).prod (λ (k : ), m - k)
theorem strict_convex_on_zpow {m : } (hm₀ : m 0) (hm₁ : m 1) :
(λ (x : ), x ^ m)

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

theorem has_deriv_at_sqrt_mul_log {x : } (hx : x 0) :
has_deriv_at (λ (x : ), x * real.log x) ((2 + real.log x) / (2 * x)) x
theorem deriv_sqrt_mul_log (x : ) :
deriv (λ (x : ), x * real.log x) x = (2 + real.log x) / (2 * x)
theorem deriv_sqrt_mul_log'  :
deriv (λ (x : ), x * real.log x) = λ (x : ), (2 + real.log x) / (2 * x)
theorem deriv2_sqrt_mul_log (x : ) :
deriv^[2] (λ (x : ), x * real.log x) x = / (4 * x ^ 3)