mathlib documentation

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 #

def convex_on (𝕜 : Type u_1) {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [has_scalar 𝕜 β] (s : set E) (f : E → β) :
Prop

Convexity of functions

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

Concavity of functions

Equations
def strict_convex_on (𝕜 : Type u_1) {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [has_scalar 𝕜 β] (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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [has_scalar 𝕜 β] (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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) :
theorem concave_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) :
theorem strict_convex_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} (hf : strict_convex_on 𝕜 s f) :
theorem strict_concave_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} (hf : strict_concave_on 𝕜 s f) :
theorem convex_on_id {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [ordered_add_comm_monoid β] [has_scalar 𝕜 β] {s : set β} (hs : convex 𝕜 s) :
convex_on 𝕜 s id
theorem concave_on_id {𝕜 : Type u_1} {β : Type u_4} [ordered_semiring 𝕜] [ordered_add_comm_monoid β] [has_scalar 𝕜 β] {s : set β} (hs : convex 𝕜 s) :
concave_on 𝕜 s id
theorem convex_on.subset {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} {t : set E} (hf : convex_on 𝕜 t f) (hst : s t) (hs : convex 𝕜 s) :
convex_on 𝕜 s f
theorem concave_on.subset {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} {t : set E} (hf : concave_on 𝕜 t f) (hst : s t) (hs : convex 𝕜 s) :
concave_on 𝕜 s f
theorem strict_convex_on.subset {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} {t : set E} (hf : strict_convex_on 𝕜 t f) (hst : s t) (hs : convex 𝕜 s) :
theorem strict_concave_on.subset {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} {t : set E} (hf : strict_concave_on 𝕜 t f) (hst : s t) (hs : convex 𝕜 s) :
theorem convex_on.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [distrib_mul_action 𝕜 β] {s : set E} {f g : E → β} (hf : convex_on 𝕜 s f) (hg : convex_on 𝕜 s g) :
convex_on 𝕜 s (f + g)
theorem concave_on.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [distrib_mul_action 𝕜 β] {s : set E} {f g : E → β} (hf : concave_on 𝕜 s f) (hg : concave_on 𝕜 s g) :
concave_on 𝕜 s (f + g)
theorem convex_on_const {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] {s : set E} (c : β) (hs : convex 𝕜 s) :
convex_on 𝕜 s (λ (x : E), c)
theorem concave_on_const {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] {s : set E} (c : β) (hs : convex 𝕜 s) :
concave_on 𝕜 s (λ (x : E), c)
theorem convex_on.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) (r : β) :
convex 𝕜 {x ∈ s | f x r}
theorem concave_on.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) (r : β) :
convex 𝕜 {x ∈ s | r f x}
theorem convex_on.convex_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) :
convex 𝕜 {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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) :
convex 𝕜 {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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} :
convex_on 𝕜 s f convex 𝕜 {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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} :
concave_on 𝕜 s f convex 𝕜 {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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} {c : E} (hf : convex_on 𝕜 s f) :
convex_on 𝕜 ((λ (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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} {c : E} (hf : concave_on 𝕜 s f) :
concave_on 𝕜 ((λ (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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} {c : E} (hf : convex_on 𝕜 s f) :
convex_on 𝕜 ((λ (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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} {c : E} (hf : concave_on 𝕜 s f) :
concave_on 𝕜 ((λ (z : E), c + z) ⁻¹' s) (f λ (z : E), z + c)

Left translation preserves strict concavity.

theorem convex_on_iff_forall_pos {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :
convex_on 𝕜 s f convex 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :
concave_on 𝕜 s f convex 𝕜 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_on_pos {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :
convex_on 𝕜 s f convex 𝕜 s s.pairwise_on (λ (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_on_pos {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :
concave_on 𝕜 s f convex 𝕜 s s.pairwise_on (λ (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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] (f : E →ₗ[𝕜] β) {s : set E} (hs : convex 𝕜 s) :
convex_on 𝕜 s f

A linear map is convex.

theorem linear_map.concave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] (f : E →ₗ[𝕜] β) {s : set E} (hs : convex 𝕜 s) :
concave_on 𝕜 s f

A linear map is concave.

theorem strict_convex_on.convex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} (hf : strict_convex_on 𝕜 s f) :
convex_on 𝕜 s f
theorem strict_concave_on.concave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} (hf : strict_concave_on 𝕜 s f) :
concave_on 𝕜 s f
theorem strict_convex_on.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_convex_on 𝕜 s f) (r : β) :
convex 𝕜 {x ∈ s | f x < r}
theorem strict_concave_on.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_concave_on 𝕜 s f) (r : β) :
convex 𝕜 {x ∈ s | r < f x}
theorem linear_order.convex_on_of_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [linear_order E] {s : set E} {f : E → β} (hs : convex 𝕜 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) :
convex_on 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [linear_order E] {s : set E} {f : E → β} (hs : convex 𝕜 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)) :
concave_on 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [linear_order E] {s : set E} {f : E → β} (hs : convex 𝕜 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) :

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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [linear_order E] {s : set E} {f : E → β} (hs : convex 𝕜 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)) :

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} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 F] [has_scalar 𝕜 β] {f : F → β} {s : set F} (hf : convex_on 𝕜 s f) (g : E →ₗ[𝕜] F) :
convex_on 𝕜 (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} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 F] [has_scalar 𝕜 β] {f : F → β} {s : set F} (hf : concave_on 𝕜 s f) (g : E →ₗ[𝕜] F) :
concave_on 𝕜 (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 {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [has_scalar 𝕜 E] [distrib_mul_action 𝕜 β] {s : set E} {f g : E → β} (hf : strict_convex_on 𝕜 s f) (hg : strict_convex_on 𝕜 s g) :
strict_convex_on 𝕜 s (f + g)
theorem strict_concave_on.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [has_scalar 𝕜 E] [distrib_mul_action 𝕜 β] {s : set E} {f g : E → β} (hf : strict_concave_on 𝕜 s f) (hg : strict_concave_on 𝕜 s g) :
strict_concave_on 𝕜 s (f + g)
theorem convex_on.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) (r : β) :
convex 𝕜 {x ∈ s | f x < r}
theorem concave_on.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) (r : β) :
convex 𝕜 {x ∈ s | r < f x}
theorem convex_on.convex_strict_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) :
convex 𝕜 {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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) :
convex 𝕜 {p : E × β | p.fst s p.snd < f p.fst}
theorem convex_on.sup {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f g : E → β} (hf : convex_on 𝕜 s f) (hg : convex_on 𝕜 s g) :
convex_on 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f g : E → β} (hf : concave_on 𝕜 s f) (hg : concave_on 𝕜 s g) :
concave_on 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f g : E → β} (hf : strict_convex_on 𝕜 s f) (hg : strict_convex_on 𝕜 s g) :
strict_convex_on 𝕜 s (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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f g : E → β} (hf : strict_concave_on 𝕜 s f) (hg : strict_concave_on 𝕜 s g) :
strict_concave_on 𝕜 s (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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 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) 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) {x y : E} (hx : x s) (hy : y s) {a b : 𝕜} (ha : 0 a) (hb : 0 b) (hab : a + b = 1) :
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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) {x y z : E} (hx : x s) (hy : y s) (hz : z [x -[𝕜] y]) :
f z 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) {x y z : E} (hx : x s) (hy : y s) (hz : z [x -[𝕜] y]) :
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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_convex_on 𝕜 s 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) < 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_concave_on 𝕜 s 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) :
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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_convex_on 𝕜 s f) {x y z : E} (hx : x s) (hy : y s) (hxy : x y) (hz : z open_segment 𝕜 x y) :
f z < 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_concave_on 𝕜 s f) {x y z : E} (hx : x s) (hy : y s) (hxy : x y) (hz : z open_segment 𝕜 x y) :
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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) {x y z : E} (hx : x s) (hy : y s) (hz : z open_segment 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) {x y z : E} (hx : x s) (hy : y s) (hz : z open_segment 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) {x y z : E} (hx : x s) (hy : y s) (hz : z open_segment 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) {x y z : E} (hx : x s) (hy : y s) (hz : z open_segment 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_convex_on 𝕜 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 strict_concave_on.left_lt_of_lt_right' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_concave_on 𝕜 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 strict_convex_on.lt_right_of_left_lt' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_convex_on 𝕜 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 strict_concave_on.lt_right_of_left_lt' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_concave_on 𝕜 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 strict_convex_on.lt_left_of_right_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_convex_on 𝕜 s f) {x y z : E} (hx : x s) (hy : y s) (hz : z open_segment 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_concave_on 𝕜 s f) {x y z : E} (hx : x s) (hy : y s) (hz : z open_segment 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_convex_on 𝕜 s f) {x y z : E} (hx : x s) (hy : y s) (hz : z open_segment 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_concave_on 𝕜 s f) {x y z : E} (hx : x s) (hy : y s) (hz : z open_segment 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_scalar 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :
convex_on 𝕜 s (-f) concave_on 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_scalar 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :
concave_on 𝕜 s (-f) convex_on 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_scalar 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :

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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_scalar 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :

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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_scalar 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :
concave_on 𝕜 s fconvex_on 𝕜 s (-f)

Alias of neg_convex_on_iff.

theorem convex_on.neg {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_scalar 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :
convex_on 𝕜 s fconcave_on 𝕜 s (-f)

Alias of neg_concave_on_iff.

theorem strict_concave_on.neg {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_scalar 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :
strict_concave_on 𝕜 s fstrict_convex_on 𝕜 s (-f)

Alias of neg_strict_convex_on_iff.

theorem strict_convex_on.neg {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_scalar 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :
strict_convex_on 𝕜 s fstrict_concave_on 𝕜 s (-f)

Alias of neg_strict_concave_on_iff.

theorem strict_convex_on.translate_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_cancel_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} {c : E} (hf : strict_convex_on 𝕜 s f) :
strict_convex_on 𝕜 ((λ (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} [ordered_semiring 𝕜] [add_cancel_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} {c : E} (hf : strict_concave_on 𝕜 s f) :
strict_concave_on 𝕜 ((λ (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} [ordered_semiring 𝕜] [add_cancel_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} {c : E} (hf : strict_convex_on 𝕜 s f) :
strict_convex_on 𝕜 ((λ (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} [ordered_semiring 𝕜] [add_cancel_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} {c : E} (hf : strict_concave_on 𝕜 s f) :
strict_concave_on 𝕜 ((λ (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} [ordered_comm_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} {c : 𝕜} (hc : 0 c) (hf : convex_on 𝕜 s f) :
convex_on 𝕜 s (λ (x : E), c f x)
theorem concave_on.smul {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_comm_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} {c : 𝕜} (hc : 0 c) (hf : concave_on 𝕜 s f) :
concave_on 𝕜 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} [linear_ordered_field 𝕜] [add_comm_group E] [add_comm_group F] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 F] [has_scalar 𝕜 β] {f : F → β} (g : E →ᵃ[𝕜] F) {s : set F} (hf : convex_on 𝕜 s f) :
convex_on 𝕜 (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} [linear_ordered_field 𝕜] [add_comm_group E] [add_comm_group F] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 F] [has_scalar 𝕜 β] {f : F → β} (g : E →ᵃ[𝕜] F) {s : set F} (hf : concave_on 𝕜 s f) :
concave_on 𝕜 (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} [linear_ordered_field 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} :
convex_on 𝕜 s f convex 𝕜 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} [linear_ordered_field 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} :
concave_on 𝕜 s f convex 𝕜 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} [linear_ordered_field 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} :
strict_convex_on 𝕜 s f convex 𝕜 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} [linear_ordered_field 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_scalar 𝕜 E] [has_scalar 𝕜 β] {s : set E} {f : E → β} :
strict_concave_on 𝕜 s f convex 𝕜 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)