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 ℝ (Set.Ici 0) 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} [LinearOrderedCommRing β] {f : α → β} [DecidablePred fun (x : α) => f x ≤ 0] {s : Finset α} (h0 : Even (Finset.filter (fun (x : α) => f x ≤ 0) s).card) : 0 ≤ Finset.prod s fun (x : α) => f x

theorem int_prod_range_nonneg (m : ℤ) (n : ℕ) (hn : Even n) : 0 ≤ Finset.prod (Finset.range n) fun (k : ℕ) => m - ↑k

theorem int_prod_range_pos {m : ℤ} {n : ℕ} (hn : Even n) (hm : m ∉ Set.Ico 0 ↑n) : 0 < Finset.prod (Finset.range n) fun (k : ℕ) => m - ↑k

theorem strictConvexOn_zpow {m : ℤ} (hm₀ : m ≠ 0) (hm₁ : m ≠ 1) : StrictConvexOn ℝ (Set.Ioi 0) 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 : ℝ) => √x * Real.log x) ((2 + Real.log x) / (2 * √x)) x

theorem deriv_sqrt_mul_log (x : ℝ) : deriv (fun (x : ℝ) => √x * Real.log x) x = (2 + Real.log x) / (2 * √x)

theorem deriv_sqrt_mul_log' : (deriv fun (x : ℝ) => √x * Real.log x) = fun (x : ℝ) => (2 + Real.log x) / (2 * √x)

theorem deriv2_sqrt_mul_log (x : ℝ) : deriv^[2] (fun (x : ℝ) => √x * Real.log x) x = -Real.log x / (4 * √x ^ 3)

theorem strictConcaveOn_sqrt_mul_log_Ioi : StrictConcaveOn ℝ (Set.Ioi 1) fun (x : ℝ) => √x * Real.log x

theorem strictConcaveOn_sin_Icc : StrictConcaveOn ℝ (Set.Icc 0 Real.pi) Real.sin

theorem strictConcaveOn_cos_Icc : StrictConcaveOn ℝ (Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) Real.cos