# Documentation

Mathlib.Analysis.Convex.SpecificFunctions.Deriv

# Collection of convex functions #

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

• Even.strictConvexOn_pow : For an even n : ℕ with 2 ≤ n, fun x => x ^ n is strictly convex.
• strictConvexOn_pow : For n : ℕ, with 2 ≤ n, fun x => x ^ n is strictly convex on $[0,+∞)$.
• strictConvexOn_zpow : For m : ℤ with m ≠ 0, 1, fun x => x ^ m is strictly convex on $[0, +∞)$.
• strictConcaveOn_sin_Icc : sin is strictly concave on $[0, π]$
• strictConcaveOn_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.SpecificFunctions.Basic.

theorem strictConvexOn_pow {n : } (hn : 2 n) :
StrictConvexOn () fun x => x ^ n

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

theorem Even.strictConvexOn_pow {n : } (hn : Even n) (h : n 0) :
StrictConvexOn Set.univ fun 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 : αβ} [DecidablePred fun x => f x 0] {s : } (h0 : Even (Finset.card (Finset.filter (fun x => f x 0) s))) :
0 Finset.prod s fun x => f x
theorem int_prod_range_nonneg (m : ) (n : ) (hn : Even n) :
0 Finset.prod () fun k => m - k
theorem int_prod_range_pos {m : } {n : } (hn : Even n) (hm : ¬m Set.Ico 0 n) :
0 < Finset.prod () fun k => m - k
theorem strictConvexOn_zpow {m : } (hm₀ : m 0) (hm₁ : m 1) :
StrictConvexOn () fun x => x ^ m

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

theorem hasDerivAt_sqrt_mul_log {x : } (hx : x 0) :
HasDerivAt (fun x => ) ((2 + ) / (2 * )) x
theorem deriv_sqrt_mul_log (x : ) :
deriv (fun x => ) x = (2 + ) / (2 * )
theorem deriv_sqrt_mul_log' :
(deriv fun x => ) = fun x => (2 + ) / (2 * )
theorem deriv2_sqrt_mul_log (x : ) :
deriv^ (fun x => ) x = / (4 * ^ 3)