# mathlib3documentation

analysis.convex.function

# Convex and concave functions #

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

This file defines convex and concave functions in vector spaces and proves the finite Jensen inequality. The integral version can be found in `analysis.convex.integral`.

A function `f : E → β` is `convex_on` a set `s` if `s` is itself a convex set, and for any two points `x y ∈ s`, the segment joining `(x, f x)` to `(y, f y)` is above the graph of `f`. Equivalently, `convex_on 𝕜 f s` means that the epigraph `{p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2}` is a convex set.

## Main declarations #

• `convex_on 𝕜 s f`: The function `f` is convex on `s` with scalars `𝕜`.
• `concave_on 𝕜 s f`: The function `f` is concave on `s` with scalars `𝕜`.
• `strict_convex_on 𝕜 s f`: The function `f` is strictly convex on `s` with scalars `𝕜`.
• `strict_concave_on 𝕜 s f`: The function `f` is strictly concave on `s` with scalars `𝕜`.
def convex_on (𝕜 : Type u_1) {E : Type u_2} {β : Type u_5} [ E] [ β] (s : set E) (f : E β) :
Prop

Convexity of functions

Equations
def concave_on (𝕜 : Type u_1) {E : Type u_2} {β : Type u_5} [ E] [ β] (s : set E) (f : E β) :
Prop

Concavity of functions

Equations
def strict_convex_on (𝕜 : Type u_1) {E : Type u_2} {β : Type u_5} [ E] [ β] (s : set E) (f : E β) :
Prop

Strict convexity of functions

Equations
def strict_concave_on (𝕜 : Type u_1) {E : Type u_2} {β : Type u_5} [ E] [ β] (s : set E) (f : E β) :
Prop

Strict concavity of functions

Equations
theorem convex_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} (hf : s f) :
s
theorem concave_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} (hf : s f) :
s
theorem strict_convex_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} (hf : f) :
theorem strict_concave_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} (hf : f) :
theorem convex_on_id {𝕜 : Type u_1} {β : Type u_5} [ β] {s : set β} (hs : s) :
s id
theorem concave_on_id {𝕜 : Type u_1} {β : Type u_5} [ β] {s : set β} (hs : s) :
s id
theorem convex_on.subset {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} {t : set E} (hf : t f) (hst : s t) (hs : s) :
s f
theorem concave_on.subset {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} {t : set E} (hf : t f) (hst : s t) (hs : s) :
s f
theorem strict_convex_on.subset {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} {t : set E} (hf : f) (hst : s t) (hs : s) :
f
theorem strict_concave_on.subset {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} {t : set E} (hf : f) (hst : s t) (hs : s) :
f
theorem convex_on.comp {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ E] [ α] [ β] {s : set E} {f : E β} {g : β α} (hg : (f '' s) g) (hf : s f) (hg' : (f '' s)) :
s (g f)
theorem concave_on.comp {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ E] [ α] [ β] {s : set E} {f : E β} {g : β α} (hg : (f '' s) g) (hf : s f) (hg' : (f '' s)) :
s (g f)
theorem convex_on.comp_concave_on {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ E] [ α] [ β] {s : set E} {f : E β} {g : β α} (hg : (f '' s) g) (hf : s f) (hg' : (f '' s)) :
s (g f)
theorem concave_on.comp_convex_on {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ E] [ α] [ β] {s : set E} {f : E β} {g : β α} (hg : (f '' s) g) (hf : s f) (hg' : (f '' s)) :
s (g f)
theorem strict_convex_on.comp {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ E] [ α] [ β] {s : set E} {f : E β} {g : β α} (hg : (f '' s) g) (hf : f) (hg' : (f '' s)) (hf' : s) :
(g f)
theorem strict_concave_on.comp {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ E] [ α] [ β] {s : set E} {f : E β} {g : β α} (hg : (f '' s) g) (hf : f) (hg' : (f '' s)) (hf' : s) :
(g f)
theorem strict_convex_on.comp_strict_concave_on {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ E] [ α] [ β] {s : set E} {f : E β} {g : β α} (hg : (f '' s) g) (hf : f) (hg' : (f '' s)) (hf' : s) :
(g f)
theorem strict_concave_on.comp_strict_convex_on {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ E] [ α] [ β] {s : set E} {f : E β} {g : β α} (hg : (f '' s) g) (hf : f) (hg' : (f '' s)) (hf' : s) :
(g f)
theorem convex_on.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f g : E β} (hf : s f) (hg : s g) :
s (f + g)
theorem concave_on.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f g : E β} (hf : s f) (hg : s g) :
s (f + g)
theorem convex_on_const {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} (c : β) (hs : s) :
s (λ (x : E), c)
theorem concave_on_const {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} (c : β) (hs : s) :
s (λ (x : E), c)
theorem convex_on_of_convex_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} (h : {p : E × β | p.fst s f p.fst p.snd}) :
s f
theorem concave_on_of_convex_hypograph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} (h : {p : E × β | p.fst s p.snd f p.fst}) :
s f
theorem convex_on.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) (r : β) :
{x ∈ s | f x r}
theorem concave_on.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) (r : β) :
{x ∈ s | r f x}
theorem convex_on.convex_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) :
{p : E × β | p.fst s f p.fst p.snd}
theorem concave_on.convex_hypograph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) :
{p : E × β | p.fst s p.snd f p.fst}
theorem convex_on_iff_convex_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} :
s f {p : E × β | p.fst s f p.fst p.snd}
theorem concave_on_iff_convex_hypograph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} :
s f {p : E × β | p.fst s p.snd f p.fst}
theorem convex_on.translate_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} (hf : s f) (c : E) :
((λ (z : E), c + z) ⁻¹' s) (f λ (z : E), c + z)

Right translation preserves convexity.

theorem concave_on.translate_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} (hf : s f) (c : E) :
((λ (z : E), c + z) ⁻¹' s) (f λ (z : E), c + z)

Right translation preserves concavity.

theorem convex_on.translate_left {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} (hf : s f) (c : E) :
((λ (z : E), c + z) ⁻¹' s) (f λ (z : E), z + c)

Left translation preserves convexity.

theorem concave_on.translate_left {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} (hf : s f) (c : E) :
((λ (z : E), c + z) ⁻¹' s) (f λ (z : E), z + c)

Left translation preserves concavity.

theorem convex_on_iff_forall_pos {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} :
s f s ⦃x : E⦄, x s ⦃y : E⦄, y s ⦃a b : 𝕜⦄, 0 < a 0 < b a + b = 1 f (a x + b y) a f x + b f y
theorem concave_on_iff_forall_pos {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} :
s f s ⦃x : E⦄, x s ⦃y : E⦄, y s ⦃a b : 𝕜⦄, 0 < a 0 < b a + b = 1 a f x + b f y f (a x + b y)
theorem convex_on_iff_pairwise_pos {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} :
s f s s.pairwise (λ (x y : E), ⦃a b : 𝕜⦄, 0 < a 0 < b a + b = 1 f (a x + b y) a f x + b f y)
theorem concave_on_iff_pairwise_pos {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} :
s f s s.pairwise (λ (x y : E), ⦃a b : 𝕜⦄, 0 < a 0 < b a + b = 1 a f x + b f y f (a x + b y))
theorem linear_map.convex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] (f : E →ₗ[𝕜] β) {s : set E} (hs : s) :
s f

A linear map is convex.

theorem linear_map.concave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] (f : E →ₗ[𝕜] β) {s : set E} (hs : s) :
s f

A linear map is concave.

theorem strict_convex_on.convex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} (hf : f) :
s f
theorem strict_concave_on.concave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} (hf : f) :
s f
theorem strict_convex_on.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : f) (r : β) :
{x ∈ s | f x < r}
theorem strict_concave_on.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : f) (r : β) :
{x ∈ s | r < f x}
theorem linear_order.convex_on_of_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [linear_order E] {s : set E} {f : E β} (hs : s) (hf : ⦃x : E⦄, x s ⦃y : E⦄, y s x < y ⦃a b : 𝕜⦄, 0 < a 0 < b a + b = 1 f (a x + b y) a f x + b f y) :
s f

For a function on a convex set in a linearly ordered space (where the order and the algebraic structures aren't necessarily compatible), in order to prove that it is convex, it suffices to verify the inequality `f (a • x + b • y) ≤ a • f x + b • f y` only for `x < y` and positive `a`, `b`. The main use case is `E = 𝕜` however one can apply it, e.g., to `𝕜^n` with lexicographic order.

theorem linear_order.concave_on_of_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [linear_order E] {s : set E} {f : E β} (hs : s) (hf : ⦃x : E⦄, x s ⦃y : E⦄, y s x < y ⦃a b : 𝕜⦄, 0 < a 0 < b a + b = 1 a f x + b f y f (a x + b y)) :
s f

For a function on a convex set in a linearly ordered space (where the order and the algebraic structures aren't necessarily compatible), in order to prove that it is concave it suffices to verify the inequality `a • f x + b • f y ≤ f (a • x + b • y)` for `x < y` and positive `a`, `b`. The main use case is `E = ℝ` however one can apply it, e.g., to `ℝ^n` with lexicographic order.

theorem linear_order.strict_convex_on_of_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [linear_order E] {s : set E} {f : E β} (hs : s) (hf : ⦃x : E⦄, x s ⦃y : E⦄, y s x < y ⦃a b : 𝕜⦄, 0 < a 0 < b a + b = 1 f (a x + b y) < a f x + b f y) :
f

For a function on a convex set in a linearly ordered space (where the order and the algebraic structures aren't necessarily compatible), in order to prove that it is strictly convex, it suffices to verify the inequality `f (a • x + b • y) < a • f x + b • f y` for `x < y` and positive `a`, `b`. The main use case is `E = 𝕜` however one can apply it, e.g., to `𝕜^n` with lexicographic order.

theorem linear_order.strict_concave_on_of_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [linear_order E] {s : set E} {f : E β} (hs : s) (hf : ⦃x : E⦄, x s ⦃y : E⦄, y s x < y ⦃a b : 𝕜⦄, 0 < a 0 < b a + b = 1 a f x + b f y < f (a x + b y)) :
f

For a function on a convex set in a linearly ordered space (where the order and the algebraic structures aren't necessarily compatible), in order to prove that it is strictly concave it suffices to verify the inequality `a • f x + b • f y < f (a • x + b • y)` for `x < y` and positive `a`, `b`. The main use case is `E = 𝕜` however one can apply it, e.g., to `𝕜^n` with lexicographic order.

theorem convex_on.comp_linear_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {β : Type u_5} [ E] [ F] [ β] {f : F β} {s : set F} (hf : s f) (g : E →ₗ[𝕜] F) :
(g ⁻¹' s) (f g)

If `g` is convex on `s`, so is `(f ∘ g)` on `f ⁻¹' s` for a linear `f`.

theorem concave_on.comp_linear_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {β : Type u_5} [ E] [ F] [ β] {f : F β} {s : set F} (hf : s f) (g : E →ₗ[𝕜] F) :
(g ⁻¹' s) (f g)

If `g` is concave on `s`, so is `(g ∘ f)` on `f ⁻¹' s` for a linear `f`.

theorem strict_convex_on.add_convex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f g : E β} (hf : f) (hg : s g) :
(f + g)
theorem convex_on.add_strict_convex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f g : E β} (hf : s f) (hg : g) :
(f + g)
theorem strict_convex_on.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f g : E β} (hf : f) (hg : g) :
(f + g)
theorem strict_concave_on.add_concave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f g : E β} (hf : f) (hg : s g) :
(f + g)
theorem concave_on.add_strict_concave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f g : E β} (hf : s f) (hg : g) :
(f + g)
theorem strict_concave_on.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f g : E β} (hf : f) (hg : g) :
(f + g)
theorem convex_on.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) (r : β) :
{x ∈ s | f x < r}
theorem concave_on.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) (r : β) :
{x ∈ s | r < f x}
theorem convex_on.open_segment_subset_strict_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) (p q : E × β) (hp : p.fst s f p.fst < p.snd) (hq : q.fst s f q.fst q.snd) :
p q {p : E × β | p.fst s f p.fst < p.snd}
theorem concave_on.open_segment_subset_strict_hypograph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) (p q : E × β) (hp : p.fst s p.snd < f p.fst) (hq : q.fst s q.snd f q.fst) :
p q {p : E × β | p.fst s p.snd < f p.fst}
theorem convex_on.convex_strict_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) :
{p : E × β | p.fst s f p.fst < p.snd}
theorem concave_on.convex_strict_hypograph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) :
{p : E × β | p.fst s p.snd < f p.fst}
theorem convex_on.sup {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f g : E β} (hf : s f) (hg : s g) :
s (f g)

The pointwise maximum of convex functions is convex.

theorem concave_on.inf {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f g : E β} (hf : s f) (hg : s g) :
s (f g)

The pointwise minimum of concave functions is concave.

theorem strict_convex_on.sup {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f g : E β} (hf : f) (hg : g) :
(f g)

The pointwise maximum of strictly convex functions is strictly convex.

theorem strict_concave_on.inf {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f g : E β} (hf : f) (hg : g) :
(f g)

The pointwise minimum of strictly concave functions is strictly concave.

theorem convex_on.le_on_segment' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y : E} (hx : x s) (hy : y s) {a b : 𝕜} (ha : 0 a) (hb : 0 b) (hab : a + b = 1) :
f (a x + b y) linear_order.max (f x) (f y)

A convex function on a segment is upper-bounded by the max of its endpoints.

theorem concave_on.ge_on_segment' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y : E} (hx : x s) (hy : y s) {a b : 𝕜} (ha : 0 a) (hb : 0 b) (hab : a + b = 1) :
linear_order.min (f x) (f y) f (a x + b y)

A concave function on a segment is lower-bounded by the min of its endpoints.

theorem convex_on.le_on_segment {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y z : E} (hx : x s) (hy : y s) (hz : z x y) :
f z linear_order.max (f x) (f y)

A convex function on a segment is upper-bounded by the max of its endpoints.

theorem concave_on.ge_on_segment {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y z : E} (hx : x s) (hy : y s) (hz : z x y) :
linear_order.min (f x) (f y) f z

A concave function on a segment is lower-bounded by the min of its endpoints.

theorem strict_convex_on.lt_on_open_segment' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : f) {x y : E} (hx : x s) (hy : y s) (hxy : x y) {a b : 𝕜} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
f (a x + b y) < linear_order.max (f x) (f y)

A strictly convex function on an open segment is strictly upper-bounded by the max of its endpoints.

theorem strict_concave_on.lt_on_open_segment' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : f) {x y : E} (hx : x s) (hy : y s) (hxy : x y) {a b : 𝕜} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
linear_order.min (f x) (f y) < f (a x + b y)

A strictly concave function on an open segment is strictly lower-bounded by the min of its endpoints.

theorem strict_convex_on.lt_on_open_segment {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : f) {x y z : E} (hx : x s) (hy : y s) (hxy : x y) (hz : z x y) :
f z < linear_order.max (f x) (f y)

A strictly convex function on an open segment is strictly upper-bounded by the max of its endpoints.

theorem strict_concave_on.lt_on_open_segment {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : f) {x y z : E} (hx : x s) (hy : y s) (hxy : x y) (hz : z x y) :
linear_order.min (f x) (f y) < f z

A strictly concave function on an open segment is strictly lower-bounded by the min of its endpoints.

theorem convex_on.le_left_of_right_le' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y : E} (hx : x s) (hy : y s) {a b : 𝕜} (ha : 0 < a) (hb : 0 b) (hab : a + b = 1) (hfy : f y f (a x + b y)) :
f (a x + b y) f x
theorem concave_on.left_le_of_le_right' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y : E} (hx : x s) (hy : y s) {a b : 𝕜} (ha : 0 < a) (hb : 0 b) (hab : a + b = 1) (hfy : f (a x + b y) f y) :
f x f (a x + b y)
theorem convex_on.le_right_of_left_le' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y : E} {a b : 𝕜} (hx : x s) (hy : y s) (ha : 0 a) (hb : 0 < b) (hab : a + b = 1) (hfx : f x f (a x + b y)) :
f (a x + b y) f y
theorem concave_on.right_le_of_le_left' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y : E} {a b : 𝕜} (hx : x s) (hy : y s) (ha : 0 a) (hb : 0 < b) (hab : a + b = 1) (hfx : f (a x + b y) f x) :
f y f (a x + b y)
theorem convex_on.le_left_of_right_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y z : E} (hx : x s) (hy : y s) (hz : z x y) (hyz : f y f z) :
f z f x
theorem concave_on.left_le_of_le_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y z : E} (hx : x s) (hy : y s) (hz : z x y) (hyz : f z f y) :
f x f z
theorem convex_on.le_right_of_left_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y z : E} (hx : x s) (hy : y s) (hz : z x y) (hxz : f x f z) :
f z f y
theorem concave_on.right_le_of_le_left {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y z : E} (hx : x s) (hy : y s) (hz : z x y) (hxz : f z f x) :
f y f z
theorem convex_on.lt_left_of_right_lt' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y : E} (hx : x s) (hy : y s) {a b : 𝕜} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hfy : f y < f (a x + b y)) :
f (a x + b y) < f x
theorem concave_on.left_lt_of_lt_right' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y : E} (hx : x s) (hy : y s) {a b : 𝕜} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hfy : f (a x + b y) < f y) :
f x < f (a x + b y)
theorem convex_on.lt_right_of_left_lt' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y : E} {a b : 𝕜} (hx : x s) (hy : y s) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hfx : f x < f (a x + b y)) :
f (a x + b y) < f y
theorem concave_on.lt_right_of_left_lt' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y : E} {a b : 𝕜} (hx : x s) (hy : y s) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hfx : f (a x + b y) < f x) :
f y < f (a x + b y)
theorem convex_on.lt_left_of_right_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y z : E} (hx : x s) (hy : y s) (hz : z x y) (hyz : f y < f z) :
f z < f x
theorem concave_on.left_lt_of_lt_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y z : E} (hx : x s) (hy : y s) (hz : z x y) (hyz : f z < f y) :
f x < f z
theorem convex_on.lt_right_of_left_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y z : E} (hx : x s) (hy : y s) (hz : z x y) (hxz : f x < f z) :
f z < f y
theorem concave_on.lt_right_of_left_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} (hf : s f) {x y z : E} (hx : x s) (hy : y s) (hz : z x y) (hxz : f z < f x) :
f y < f z
@[simp]
theorem neg_convex_on_iff {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} :
s (-f) s f

A function `-f` is convex iff `f` is concave.

@[simp]
theorem neg_concave_on_iff {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} :
s (-f) s f

A function `-f` is concave iff `f` is convex.

@[simp]
theorem neg_strict_convex_on_iff {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} :
(-f) f

A function `-f` is strictly convex iff `f` is strictly concave.

@[simp]
theorem neg_strict_concave_on_iff {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} :
(-f) f

A function `-f` is strictly concave iff `f` is strictly convex.

theorem concave_on.neg {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} :
s f s (-f)

Alias of the reverse direction of `neg_convex_on_iff`.

theorem convex_on.neg {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} :
s f s (-f)

Alias of the reverse direction of `neg_concave_on_iff`.

theorem strict_concave_on.neg {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} :
f (-f)

Alias of the reverse direction of `neg_strict_convex_on_iff`.

theorem strict_convex_on.neg {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} :
f (-f)

Alias of the reverse direction of `neg_strict_concave_on_iff`.

theorem convex_on.sub {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f g : E β} (hf : s f) (hg : s g) :
s (f - g)
theorem concave_on.sub {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f g : E β} (hf : s f) (hg : s g) :
s (f - g)
theorem strict_convex_on.sub {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f g : E β} (hf : f) (hg : g) :
(f - g)
theorem strict_concave_on.sub {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f g : E β} (hf : f) (hg : g) :
(f - g)
theorem convex_on.sub_strict_concave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f g : E β} (hf : s f) (hg : g) :
(f - g)
theorem concave_on.sub_strict_convex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f g : E β} (hf : s f) (hg : g) :
(f - g)
theorem strict_convex_on.sub_concave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f g : E β} (hf : f) (hg : s g) :
(f - g)
theorem strict_concave_on.sub_convex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f g : E β} (hf : f) (hg : s g) :
(f - g)
theorem strict_convex_on.translate_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} (hf : f) (c : E) :
((λ (z : E), c + z) ⁻¹' s) (f λ (z : E), c + z)

Right translation preserves strict convexity.

theorem strict_concave_on.translate_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} (hf : f) (c : E) :
((λ (z : E), c + z) ⁻¹' s) (f λ (z : E), c + z)

Right translation preserves strict concavity.

theorem strict_convex_on.translate_left {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} (hf : f) (c : E) :
((λ (z : E), c + z) ⁻¹' s) (f λ (z : E), z + c)

Left translation preserves strict convexity.

theorem strict_concave_on.translate_left {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} (hf : f) (c : E) :
((λ (z : E), c + z) ⁻¹' s) (f λ (z : E), z + c)

Left translation preserves strict concavity.

theorem convex_on.smul {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} {c : 𝕜} (hc : 0 c) (hf : s f) :
s (λ (x : E), c f x)
theorem concave_on.smul {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] [ β] {s : set E} {f : E β} {c : 𝕜} (hc : 0 c) (hf : s f) :
s (λ (x : E), c f x)
theorem convex_on.comp_affine_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {β : Type u_5} [ E] [ F] [ β] {f : F β} (g : E →ᵃ[𝕜] F) {s : set F} (hf : s f) :
(g ⁻¹' s) (f g)

If a function is convex on `s`, it remains convex when precomposed by an affine map.

theorem concave_on.comp_affine_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {β : Type u_5} [ E] [ F] [ β] {f : F β} (g : E →ᵃ[𝕜] F) {s : set F} (hf : s f) :
(g ⁻¹' s) (f g)

If a function is concave on `s`, it remains concave when precomposed by an affine map.

theorem convex_on_iff_div {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} :
s f s ⦃x : E⦄, x s ⦃y : E⦄, y s ⦃a b : 𝕜⦄, 0 a 0 b 0 < a + b f ((a / (a + b)) x + (b / (a + b)) y) (a / (a + b)) f x + (b / (a + b)) f y
theorem concave_on_iff_div {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} :
s f s ⦃x : E⦄, x s ⦃y : E⦄, y s ⦃a b : 𝕜⦄, 0 a 0 b 0 < a + b (a / (a + b)) f x + (b / (a + b)) f y f ((a / (a + b)) x + (b / (a + b)) y)
theorem strict_convex_on_iff_div {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} :
f s ⦃x : E⦄, x s ⦃y : E⦄, y s x y ⦃a b : 𝕜⦄, 0 < a 0 < b f ((a / (a + b)) x + (b / (a + b)) y) < (a / (a + b)) f x + (b / (a + b)) f y
theorem strict_concave_on_iff_div {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ E] [ β] {s : set E} {f : E β} :
f s ⦃x : E⦄, x s ⦃y : E⦄, y s x y ⦃a b : 𝕜⦄, 0 < a 0 < b (a / (a + b)) f x + (b / (a + b)) f y < f ((a / (a + b)) x + (b / (a + b)) y)
theorem convex_on.le_right_of_left_le'' {𝕜 : Type u_1} {β : Type u_5} [ β] [ β] {x y z : 𝕜} {s : set 𝕜} {f : 𝕜 β} (hf : s f) (hx : x s) (hz : z s) (hxy : x < y) (hyz : y z) (h : f x f y) :
f y f z
theorem convex_on.le_left_of_right_le'' {𝕜 : Type u_1} {β : Type u_5} [ β] [ β] {x y z : 𝕜} {s : set 𝕜} {f : 𝕜 β} (hf : s f) (hx : x s) (hz : z s) (hxy : x y) (hyz : y < z) (h : f z f y) :
f y f x
theorem concave_on.right_le_of_le_left'' {𝕜 : Type u_1} {β : Type u_5} [ β] [ β] {x y z : 𝕜} {s : set 𝕜} {f : 𝕜 β} (hf : s f) (hx : x s) (hz : z s) (hxy : x < y) (hyz : y z) (h : f y f x) :
f z f y
theorem concave_on.left_le_of_le_right'' {𝕜 : Type u_1} {β : Type u_5} [ β] [ β] {x y z : 𝕜} {s : set 𝕜} {f : 𝕜 β} (hf : s f) (hx : x s) (hz : z s) (hxy : x y) (hyz : y < z) (h : f y f z) :
f x f y