mathlib3 documentation

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 #

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

Convexity of functions

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

Concavity of functions

Equations
def strict_convex_on (𝕜 : Type u_1) {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] (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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] (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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E β} (hf : convex_on 𝕜 s f) :
theorem concave_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E β} (hf : concave_on 𝕜 s f) :
theorem strict_convex_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E β} (hf : strict_concave_on 𝕜 s f) :
theorem convex_on_id {𝕜 : Type u_1} {β : Type u_5} [ordered_semiring 𝕜] [ordered_add_comm_monoid β] [has_smul 𝕜 β] {s : set β} (hs : convex 𝕜 s) :
convex_on 𝕜 s id
theorem concave_on_id {𝕜 : Type u_1} {β : Type u_5} [ordered_semiring 𝕜] [ordered_add_comm_monoid β] [has_smul 𝕜 β] {s : set β} (hs : convex 𝕜 s) :
concave_on 𝕜 s id
theorem convex_on.subset {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E β} {t : set E} (hf : strict_concave_on 𝕜 t f) (hst : s t) (hs : convex 𝕜 s) :
theorem convex_on.comp {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 α] [has_smul 𝕜 β] {s : set E} {f : E β} {g : β α} (hg : convex_on 𝕜 (f '' s) g) (hf : convex_on 𝕜 s f) (hg' : monotone_on g (f '' s)) :
convex_on 𝕜 s (g f)
theorem concave_on.comp {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 α] [has_smul 𝕜 β] {s : set E} {f : E β} {g : β α} (hg : concave_on 𝕜 (f '' s) g) (hf : concave_on 𝕜 s f) (hg' : monotone_on g (f '' s)) :
concave_on 𝕜 s (g f)
theorem convex_on.comp_concave_on {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 α] [has_smul 𝕜 β] {s : set E} {f : E β} {g : β α} (hg : convex_on 𝕜 (f '' s) g) (hf : concave_on 𝕜 s f) (hg' : antitone_on g (f '' s)) :
convex_on 𝕜 s (g f)
theorem concave_on.comp_convex_on {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 α] [has_smul 𝕜 β] {s : set E} {f : E β} {g : β α} (hg : concave_on 𝕜 (f '' s) g) (hf : convex_on 𝕜 s f) (hg' : antitone_on g (f '' s)) :
concave_on 𝕜 s (g f)
theorem strict_convex_on.comp {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 α] [has_smul 𝕜 β] {s : set E} {f : E β} {g : β α} (hg : strict_convex_on 𝕜 (f '' s) g) (hf : strict_convex_on 𝕜 s f) (hg' : strict_mono_on g (f '' s)) (hf' : set.inj_on f s) :
strict_convex_on 𝕜 s (g f)
theorem strict_concave_on.comp {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 α] [has_smul 𝕜 β] {s : set E} {f : E β} {g : β α} (hg : strict_concave_on 𝕜 (f '' s) g) (hf : strict_concave_on 𝕜 s f) (hg' : strict_mono_on g (f '' s)) (hf' : set.inj_on f s) :
strict_concave_on 𝕜 s (g f)
theorem strict_convex_on.comp_strict_concave_on {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 α] [has_smul 𝕜 β] {s : set E} {f : E β} {g : β α} (hg : strict_convex_on 𝕜 (f '' s) g) (hf : strict_concave_on 𝕜 s f) (hg' : strict_anti_on g (f '' s)) (hf' : set.inj_on f s) :
strict_convex_on 𝕜 s (g f)
theorem strict_concave_on.comp_strict_convex_on {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 α] [has_smul 𝕜 β] {s : set E} {f : E β} {g : β α} (hg : strict_concave_on 𝕜 (f '' s) g) (hf : strict_convex_on 𝕜 s f) (hg' : strict_anti_on g (f '' s)) (hf' : set.inj_on f s) :
strict_concave_on 𝕜 s (g f)
theorem convex_on.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} (c : β) (hs : convex 𝕜 s) :
concave_on 𝕜 s (λ (x : E), c)
theorem convex_on_of_convex_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f : E β} (h : convex 𝕜 {p : E × β | p.fst s f p.fst p.snd}) :
convex_on 𝕜 s f
theorem concave_on_of_convex_hypograph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f : E β} (h : convex 𝕜 {p : E × β | p.fst s p.snd f p.fst}) :
concave_on 𝕜 s f
theorem convex_on.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E β} (hf : convex_on 𝕜 s f) (c : E) :
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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E β} (hf : concave_on 𝕜 s f) (c : E) :
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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E β} (hf : convex_on 𝕜 s f) (c : E) :
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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E β} (hf : concave_on 𝕜 s f) (c : E) :
concave_on 𝕜 ((λ (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} [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 : 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} [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 : 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} [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 (λ (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} [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 (λ (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} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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 : 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) :
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_5} [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 : 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)) :
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_5} [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 : 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) :

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} [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 : 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)) :

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} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 F] [has_smul 𝕜 β] {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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 F] [has_smul 𝕜 β] {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_convex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [has_smul 𝕜 E] [distrib_mul_action 𝕜 β] {s : set E} {f g : E β} (hf : strict_convex_on 𝕜 s f) (hg : convex_on 𝕜 s g) :
strict_convex_on 𝕜 s (f + g)
theorem convex_on.add_strict_convex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [has_smul 𝕜 E] [distrib_mul_action 𝕜 β] {s : set E} {f g : E β} (hf : convex_on 𝕜 s f) (hg : strict_convex_on 𝕜 s g) :
strict_convex_on 𝕜 s (f + g)
theorem strict_convex_on.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [has_smul 𝕜 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_concave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [has_smul 𝕜 E] [distrib_mul_action 𝕜 β] {s : set E} {f g : E β} (hf : strict_concave_on 𝕜 s f) (hg : concave_on 𝕜 s g) :
strict_concave_on 𝕜 s (f + g)
theorem concave_on.add_strict_concave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [has_smul 𝕜 E] [distrib_mul_action 𝕜 β] {s : set E} {f g : E β} (hf : concave_on 𝕜 s f) (hg : strict_concave_on 𝕜 s g) :
strict_concave_on 𝕜 s (f + g)
theorem strict_concave_on.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [has_smul 𝕜 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_5} [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_5} [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.open_segment_subset_strict_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [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) (p q : E × β) (hp : p.fst s f p.fst < p.snd) (hq : q.fst s f q.fst q.snd) :
open_segment 𝕜 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} [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) (p q : E × β) (hp : p.fst s p.snd < f p.fst) (hq : q.fst s q.snd f q.fst) :
open_segment 𝕜 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} [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_5} [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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 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) 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 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) :
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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 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 segment 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 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 segment 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 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) < 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 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) :
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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 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 < 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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 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) :
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} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_smul 𝕜 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.right_le_of_le_left' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_smul 𝕜 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.right_le_of_le_left {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_smul 𝕜 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 convex_on.lt_left_of_right_lt' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 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_lt_of_lt_right' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 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.lt_right_of_left_lt' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 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.lt_right_of_left_lt' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 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.lt_left_of_right_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 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_lt_of_lt_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 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.lt_right_of_left_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 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.lt_right_of_left_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 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
@[simp]
theorem neg_convex_on_iff {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 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_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f : E β} :
concave_on 𝕜 s f convex_on 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f : E β} :
convex_on 𝕜 s f concave_on 𝕜 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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f : E β} :

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

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} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f g : E β} (hf : convex_on 𝕜 s f) (hg : concave_on 𝕜 s g) :
convex_on 𝕜 s (f - g)
theorem concave_on.sub {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f g : E β} (hf : concave_on 𝕜 s f) (hg : convex_on 𝕜 s g) :
concave_on 𝕜 s (f - g)
theorem strict_convex_on.sub {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f g : E β} (hf : strict_convex_on 𝕜 s f) (hg : strict_concave_on 𝕜 s g) :
strict_convex_on 𝕜 s (f - g)
theorem strict_concave_on.sub {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f g : E β} (hf : strict_concave_on 𝕜 s f) (hg : strict_convex_on 𝕜 s g) :
strict_concave_on 𝕜 s (f - g)
theorem convex_on.sub_strict_concave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f g : E β} (hf : convex_on 𝕜 s f) (hg : strict_concave_on 𝕜 s g) :
strict_convex_on 𝕜 s (f - g)
theorem concave_on.sub_strict_convex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f g : E β} (hf : concave_on 𝕜 s f) (hg : strict_convex_on 𝕜 s g) :
strict_concave_on 𝕜 s (f - g)
theorem strict_convex_on.sub_concave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f g : E β} (hf : strict_convex_on 𝕜 s f) (hg : concave_on 𝕜 s g) :
strict_convex_on 𝕜 s (f - g)
theorem strict_concave_on.sub_convex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f g : E β} (hf : strict_concave_on 𝕜 s f) (hg : convex_on 𝕜 s g) :
strict_concave_on 𝕜 s (f - g)
theorem strict_convex_on.translate_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_cancel_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E β} (hf : strict_convex_on 𝕜 s f) (c : E) :
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_5} [ordered_semiring 𝕜] [add_cancel_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E β} (hf : strict_concave_on 𝕜 s f) (c : E) :
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_5} [ordered_semiring 𝕜] [add_cancel_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E β} (hf : strict_convex_on 𝕜 s f) (c : E) :
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_5} [ordered_semiring 𝕜] [add_cancel_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E β} (hf : strict_concave_on 𝕜 s f) (c : E) :
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_5} [ordered_comm_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 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_5} [ordered_comm_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 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_5} [linear_ordered_field 𝕜] [add_comm_group E] [add_comm_group F] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 F] [has_smul 𝕜 β] {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_5} [linear_ordered_field 𝕜] [add_comm_group E] [add_comm_group F] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 F] [has_smul 𝕜 β] {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_5} [linear_ordered_field 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E β} :
convex_on 𝕜 s f convex 𝕜 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} [linear_ordered_field 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E β} :
concave_on 𝕜 s f convex 𝕜 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} [linear_ordered_field 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E β} :
strict_convex_on 𝕜 s f convex 𝕜 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} [linear_ordered_field 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E β} :
strict_concave_on 𝕜 s f convex 𝕜 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} [linear_ordered_field 𝕜] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] {x y z : 𝕜} {s : set 𝕜} {f : 𝕜 β} (hf : convex_on 𝕜 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} [linear_ordered_field 𝕜] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] {x y z : 𝕜} {s : set 𝕜} {f : 𝕜 β} (hf : convex_on 𝕜 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} [linear_ordered_field 𝕜] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] {x y z : 𝕜} {s : set 𝕜} {f : 𝕜 β} (hf : concave_on 𝕜 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} [linear_ordered_field 𝕜] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] {x y z : 𝕜} {s : set 𝕜} {f : 𝕜 β} (hf : concave_on 𝕜 s f) (hx : x s) (hz : z s) (hxy : x y) (hyz : y < z) (h : f y f z) :
f x f y