# mathlibdocumentation

analysis.convex.function

# Convex and concave functions #

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_4} [ E] [ β] (s : set E) (f : E → β) :
Prop

Convexity of functions

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

Concavity of functions

Equations
def strict_convex_on (𝕜 : Type u_1) {E : Type u_2} {β : Type u_4} [ 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_4} [ 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_4} [ E] [ β] {s : set E} {f : E → β} (hf : s f) :
s
theorem concave_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ E] [ β] {s : set E} {f : E → β} (hf : s f) :
s
theorem strict_convex_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ E] [ β] {s : set E} {f : E → β} (hf : f) :
theorem strict_concave_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ E] [ β] {s : set E} {f : E → β} (hf : f) :
theorem convex_on_id {𝕜 : Type u_1} {β : Type u_4} [ β] {s : set β} (hs : s) :
s id
theorem concave_on_id {𝕜 : Type u_1} {β : Type u_4} [ β] {s : set β} (hs : s) :
s id
theorem convex_on.subset {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ 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_4} [ 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_4} [ 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_4} [ E] [ β] {s : set E} {f : E → β} {t : set E} (hf : f) (hst : s t) (hs : s) :
f
theorem convex_on.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ 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_4} [ 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_4} [ E] [ β] {s : set E} (c : β) (hs : s) :
s (λ (x : E), c)
theorem concave_on_const {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ E] [ β] {s : set E} {f : E → β} :
s f s ∀ ⦃x y : E⦄, x sy s∀ ⦃a b : 𝕜⦄, 0 < a0 < ba + b = 1f (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_4} [ E] [ β] {s : set E} {f : E → β} :
s f s ∀ ⦃x y : E⦄, x sy s∀ ⦃a b : 𝕜⦄, 0 < a0 < ba + b = 1a 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_4} [ E] [ β] {s : set E} {f : E → β} :
s f s s.pairwise (λ (x y : E), ∀ ⦃a b : 𝕜⦄, 0 < a0 < ba + b = 1f (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_4} [ E] [ β] {s : set E} {f : E → β} :
s f s s.pairwise (λ (x y : E), ∀ ⦃a b : 𝕜⦄, 0 < a0 < ba + b = 1a f x + b f y f (a x + b y))
theorem linear_map.convex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ E] [ β] [linear_order E] {s : set E} {f : E → β} (hs : s) (hf : ∀ ⦃x y : E⦄, x sy sx < y∀ ⦃a b : 𝕜⦄, 0 < a0 < ba + b = 1f (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_4} [ E] [ β] [linear_order E] {s : set E} {f : E → β} (hs : s) (hf : ∀ ⦃x y : E⦄, x sy sx < y∀ ⦃a b : 𝕜⦄, 0 < a0 < ba + b = 1a 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_4} [ E] [ β] [linear_order E] {s : set E} {f : E → β} (hs : s) (hf : ∀ ⦃x y : E⦄, x sy sx < y∀ ⦃a b : 𝕜⦄, 0 < a0 < ba + b = 1f (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 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_4} [ E] [ β] [linear_order E] {s : set E} {f : E → β} (hs : s) (hf : ∀ ⦃x y : E⦄, x sy sx < y∀ ⦃a b : 𝕜⦄, 0 < a0 < ba + b = 1a 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 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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.le_right_of_left_le' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ 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_4} [ 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_4} [ 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_4} [ 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.le_right_of_left_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ 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 strict_convex_on.lt_left_of_right_lt' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ E] [ β] [ β] {s : set E} {f : E → β} (hf : 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 strict_concave_on.left_lt_of_lt_right' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ E] [ β] [ β] {s : set E} {f : E → β} (hf : 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 strict_convex_on.lt_right_of_left_lt' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ E] [ β] [ β] {s : set E} {f : E → β} (hf : 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 strict_concave_on.lt_right_of_left_lt' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ E] [ β] [ β] {s : set E} {f : E → β} (hf : 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 strict_convex_on.lt_left_of_right_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ E] [ β] [ β] {s : set E} {f : E → β} (hf : 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 strict_concave_on.left_lt_of_lt_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ E] [ β] [ β] {s : set E} {f : E → β} (hf : 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 strict_convex_on.lt_right_of_left_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ E] [ β] [ β] {s : set E} {f : E → β} (hf : 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 strict_concave_on.lt_right_of_left_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ E] [ β] [ β] {s : set E} {f : E → β} (hf : 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ 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_4} [ E] [ β] {s : set E} {f : E → β} :
s f s ∀ ⦃x y : E⦄, x sy s∀ ⦃a b : 𝕜⦄, 0 a0 b0 < a + bf ((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_4} [ E] [ β] {s : set E} {f : E → β} :
s f s ∀ ⦃x y : E⦄, x sy s∀ ⦃a b : 𝕜⦄, 0 a0 b0 < 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_4} [ E] [ β] {s : set E} {f : E → β} :
f s ∀ ⦃x y : E⦄, x sy sx y∀ ⦃a b : 𝕜⦄, 0 < a0 < bf ((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_4} [ E] [ β] {s : set E} {f : E → β} :
f s ∀ ⦃x y : E⦄, x sy sx y∀ ⦃a b : 𝕜⦄, 0 < a0 < b(a / (a + b)) f x + (b / (a + b)) f y < f ((a / (a + b)) x + (b / (a + b)) y)