Convex and concave functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines convex and concave functions in vector spaces and proves the finite Jensen
inequality. The integral version can be found in analysis.convex.integral.
A function f : E → β is convex_on a set s if s is itself a convex set, and for any two
points x y ∈ s, the segment joining (x, f x) to (y, f y) is above the graph of f.
Equivalently, convex_on 𝕜 f s means that the epigraph {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} is
a convex set.
Main declarations #
convex_on 𝕜 s f: The functionfis convex onswith scalars𝕜.concave_on 𝕜 s f: The functionfis concave onswith scalars𝕜.strict_convex_on 𝕜 s f: The functionfis strictly convex onswith scalars𝕜.strict_concave_on 𝕜 s f: The functionfis strictly concave onswith scalars𝕜.
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
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
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
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
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) :
concave_on 𝕜 s (⇑order_dual.to_dual ∘ 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) :
convex_on 𝕜 s (⇑order_dual.to_dual ∘ 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) :
strict_concave_on 𝕜 s (⇑order_dual.to_dual ∘ 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) :
strict_convex_on 𝕜 s (⇑order_dual.to_dual ∘ f)
theorem
convex_on_id
{𝕜 : Type u_1}
{β : Type u_5}
[ordered_semiring 𝕜]
[ordered_add_comm_monoid β]
[has_smul 𝕜 β]
{s : set β}
(hs : convex 𝕜 s) :
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) :
strict_convex_on 𝕜 s f
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) :
strict_concave_on 𝕜 s f
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)) :
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)) :
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) :
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
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 : β) :
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 : β) :
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) :
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) :
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 → β} :
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 → β} :
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) :
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) :
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 → β} :
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 → β} :
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 → β} :
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 → β} :
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) :
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 : β) :
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 : β) :
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) :
strict_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 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)) :
strict_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 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) :
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 : β) :
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 : β) :
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) :
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) :
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) :
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) :
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) :
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)) :
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) :
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)) :
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) :
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)) :
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) :
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)) :
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) :
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 → β} :
strict_convex_on 𝕜 s (-f) ↔ strict_concave_on 𝕜 s f
A function -f is strictly convex iff f is strictly concave.
@[simp]
theorem
neg_strict_concave_on_iff
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_5}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[ordered_add_comm_group β]
[has_smul 𝕜 E]
[module 𝕜 β]
{s : set E}
{f : E → β} :
strict_concave_on 𝕜 s (-f) ↔ strict_convex_on 𝕜 s f
A function -f is strictly concave iff f is strictly convex.
theorem
concave_on.neg
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_5}
[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 → β} :
strict_concave_on 𝕜 s f → strict_convex_on 𝕜 s (-f)
Alias of the reverse direction of neg_strict_convex_on_iff.
theorem
strict_convex_on.neg
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_5}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[ordered_add_comm_group β]
[has_smul 𝕜 E]
[module 𝕜 β]
{s : set E}
{f : E → β} :
strict_convex_on 𝕜 s f → strict_concave_on 𝕜 s (-f)
Alias of the reverse direction of neg_strict_concave_on_iff.
theorem
convex_on.sub
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_5}
[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) :
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) :
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) :
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 → β} :
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 → β} :
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 → β} :
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 → β} :
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