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 evenn : ℕwith2 ≤ n,λ x, x ^ nis strictly convex.strict_convex_on_pow: Forn : ℕ, with2 ≤ n,λ x, x ^ nis strictly convex on $[0, +∞)$.strict_convex_on_zpow: Form : ℤwithm ≠ 0, 1,λ x, x ^ mis strictly convex on $[0, +∞)$.strict_concave_on_sin_Icc:sinis strictly concave on $[0, π]$strict_concave_on_cos_Icc:cosis 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) :
strict_convex_on ℝ (set.Ici 0) (λ (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) :
strict_convex_on ℝ set.univ (λ (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}
[linear_ordered_comm_ring β]
{f : α → β}
[decidable_pred (λ (x : α), f x ≤ 0)]
{s : finset α}
(h0 : even (finset.filter (λ (x : α), f x ≤ 0) s).card) :
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.