Collection of convex functions #
In this file we prove that the following functions are convex:
strict_convex_on_exp
: The exponential function is strictly convex.even.convex_on_pow
,even.strict_convex_on_pow
: For an evenn : ℕ
,λ x, x ^ n
is convex and strictly convex when2 ≤ n
.convex_on_pow
,strict_convex_on_pow
: Forn : ℕ
,λ x, x ^ n
is convex on $[0, +∞)$ and strictly convex when2 ≤ n
.convex_on_zpow
,strict_convex_on_zpow
: Form : ℤ
,λ x, x ^ m
is convex on $[0, +∞)$ and strictly convex whenm ≠ 0, 1
.convex_on_rpow
,strict_convex_on_rpow
: Forp : ℝ
,λ x, x ^ p
is convex on $[0, +∞)$ when1 ≤ p
and strictly convex when1 < p
.strict_concave_on_log_Ioi
,strict_concave_on_log_Iio
:real.log
is strictly concave on $(0, +∞)$ and $(-∞, 0)$ respectively.
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.
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
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
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
.
theorem
strict_convex_on_rpow
{p : ℝ}
(hp : 1 < p) :
strict_convex_on ℝ (set.Ici 0) (λ (x : ℝ), x ^ p)