Quasiconvex and quasiconcave functions #
This file defines quasiconvexity, quasiconcavity and quasilinearity of functions, which are generalizations of unimodality and monotonicity. Convexity implies quasiconvexity, concavity implies quasiconcavity, and monotonicity implies quasilinearity.
Main declarations #
quasiconvex_on 𝕜 s f
: Quasiconvexity of the functionf
on the sets
with scalars𝕜
. This means that, for allr
,{x ∈ s | f x ≤ r}
is𝕜
-convex.quasiconcave_on 𝕜 s f
: Quasiconcavity of the functionf
on the sets
with scalars𝕜
. This means that, for allr
,{x ∈ s | r ≤ f x}
is𝕜
-convex.quasilinear_on 𝕜 s f
: Quasilinearity of the functionf
on the sets
with scalars𝕜
. This means thatf
is both quasiconvex and quasiconcave.
References #
def
quasiconvex_on
(𝕜 : Type u_1)
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[ordered_add_comm_monoid β]
[has_smul 𝕜 E]
(s : set E)
(f : E → β) :
Prop
A function is quasiconvex if all its sublevels are convex.
This means that, for all r
, {x ∈ s | f x ≤ r}
is 𝕜
-convex.
Equations
- quasiconvex_on 𝕜 s f = ∀ (r : β), convex 𝕜 {x ∈ s | f x ≤ r}
def
quasiconcave_on
(𝕜 : Type u_1)
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[ordered_add_comm_monoid β]
[has_smul 𝕜 E]
(s : set E)
(f : E → β) :
Prop
A function is quasiconcave if all its superlevels are convex.
This means that, for all r
, {x ∈ s | r ≤ f x}
is 𝕜
-convex.
Equations
- quasiconcave_on 𝕜 s f = ∀ (r : β), convex 𝕜 {x ∈ s | r ≤ f x}
def
quasilinear_on
(𝕜 : Type u_1)
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[ordered_add_comm_monoid β]
[has_smul 𝕜 E]
(s : set E)
(f : E → β) :
Prop
A function is quasilinear if it is both quasiconvex and quasiconcave.
This means that, for all r
,
the sets {x ∈ s | f x ≤ r}
and {x ∈ s | r ≤ f x}
are 𝕜
-convex.
Equations
- quasilinear_on 𝕜 s f = (quasiconvex_on 𝕜 s f ∧ quasiconcave_on 𝕜 s f)
theorem
quasiconvex_on.dual
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[ordered_add_comm_monoid β]
[has_smul 𝕜 E]
{s : set E}
{f : E → β} :
quasiconvex_on 𝕜 s f → quasiconcave_on 𝕜 s (⇑order_dual.to_dual ∘ f)
theorem
quasiconcave_on.dual
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[ordered_add_comm_monoid β]
[has_smul 𝕜 E]
{s : set E}
{f : E → β} :
quasiconcave_on 𝕜 s f → quasiconvex_on 𝕜 s (⇑order_dual.to_dual ∘ f)
theorem
quasilinear_on.dual
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[ordered_add_comm_monoid β]
[has_smul 𝕜 E]
{s : set E}
{f : E → β} :
quasilinear_on 𝕜 s f → quasilinear_on 𝕜 s (⇑order_dual.to_dual ∘ f)
theorem
convex.quasiconvex_on_of_convex_le
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[ordered_add_comm_monoid β]
[has_smul 𝕜 E]
{s : set E}
{f : E → β}
(hs : convex 𝕜 s)
(h : ∀ (r : β), convex 𝕜 {x : E | f x ≤ r}) :
quasiconvex_on 𝕜 s f
theorem
convex.quasiconcave_on_of_convex_ge
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[ordered_add_comm_monoid β]
[has_smul 𝕜 E]
{s : set E}
{f : E → β}
(hs : convex 𝕜 s)
(h : ∀ (r : β), convex 𝕜 {x : E | r ≤ f x}) :
quasiconcave_on 𝕜 s f
theorem
quasiconvex_on.convex
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[ordered_add_comm_monoid β]
[has_smul 𝕜 E]
{s : set E}
{f : E → β}
[is_directed β has_le.le]
(hf : quasiconvex_on 𝕜 s f) :
convex 𝕜 s
theorem
quasiconcave_on.convex
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[ordered_add_comm_monoid β]
[has_smul 𝕜 E]
{s : set E}
{f : E → β}
[is_directed β ge]
(hf : quasiconcave_on 𝕜 s f) :
convex 𝕜 s
theorem
quasiconvex_on.sup
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[linear_ordered_add_comm_monoid β]
[has_smul 𝕜 E]
{s : set E}
{f g : E → β}
(hf : quasiconvex_on 𝕜 s f)
(hg : quasiconvex_on 𝕜 s g) :
quasiconvex_on 𝕜 s (f ⊔ g)
theorem
quasiconcave_on.inf
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[linear_ordered_add_comm_monoid β]
[has_smul 𝕜 E]
{s : set E}
{f g : E → β}
(hf : quasiconcave_on 𝕜 s f)
(hg : quasiconcave_on 𝕜 s g) :
quasiconcave_on 𝕜 s (f ⊓ g)
theorem
quasiconvex_on_iff_le_max
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[linear_ordered_add_comm_monoid β]
[has_smul 𝕜 E]
{s : set E}
{f : E → β} :
theorem
quasiconcave_on_iff_min_le
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[linear_ordered_add_comm_monoid β]
[has_smul 𝕜 E]
{s : set E}
{f : E → β} :
theorem
quasilinear_on_iff_mem_uIcc
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[linear_ordered_add_comm_monoid β]
[has_smul 𝕜 E]
{s : set E}
{f : E → β} :
theorem
quasiconvex_on.convex_lt
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[linear_ordered_add_comm_monoid β]
[has_smul 𝕜 E]
{s : set E}
{f : E → β}
(hf : quasiconvex_on 𝕜 s f)
(r : β) :
theorem
quasiconcave_on.convex_gt
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[linear_ordered_add_comm_monoid β]
[has_smul 𝕜 E]
{s : set E}
{f : E → β}
(hf : quasiconcave_on 𝕜 s f)
(r : β) :
theorem
convex_on.quasiconvex_on
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[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) :
quasiconvex_on 𝕜 s f
theorem
concave_on.quasiconcave_on
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[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) :
quasiconcave_on 𝕜 s f
theorem
monotone_on.quasiconvex_on
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{s : set E}
{f : E → β}
(hf : monotone_on f s)
(hs : convex 𝕜 s) :
quasiconvex_on 𝕜 s f
theorem
monotone_on.quasiconcave_on
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{s : set E}
{f : E → β}
(hf : monotone_on f s)
(hs : convex 𝕜 s) :
quasiconcave_on 𝕜 s f
theorem
monotone_on.quasilinear_on
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{s : set E}
{f : E → β}
(hf : monotone_on f s)
(hs : convex 𝕜 s) :
quasilinear_on 𝕜 s f
theorem
antitone_on.quasiconvex_on
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{s : set E}
{f : E → β}
(hf : antitone_on f s)
(hs : convex 𝕜 s) :
quasiconvex_on 𝕜 s f
theorem
antitone_on.quasiconcave_on
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{s : set E}
{f : E → β}
(hf : antitone_on f s)
(hs : convex 𝕜 s) :
quasiconcave_on 𝕜 s f
theorem
antitone_on.quasilinear_on
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{s : set E}
{f : E → β}
(hf : antitone_on f s)
(hs : convex 𝕜 s) :
quasilinear_on 𝕜 s f
theorem
monotone.quasiconvex_on
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{f : E → β}
(hf : monotone f) :
theorem
monotone.quasiconcave_on
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{f : E → β}
(hf : monotone f) :
theorem
monotone.quasilinear_on
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{f : E → β}
(hf : monotone f) :
theorem
antitone.quasiconvex_on
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{f : E → β}
(hf : antitone f) :
theorem
antitone.quasiconcave_on
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{f : E → β}
(hf : antitone f) :
theorem
antitone.quasilinear_on
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid β]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{f : E → β}
(hf : antitone f) :
theorem
quasilinear_on.monotone_on_or_antitone_on
{𝕜 : Type u_1}
{β : Type u_4}
[linear_ordered_field 𝕜]
[linear_ordered_add_comm_monoid β]
{s : set 𝕜}
{f : 𝕜 → β}
(hf : quasilinear_on 𝕜 s f) :
monotone_on f s ∨ antitone_on f s
theorem
quasilinear_on_iff_monotone_on_or_antitone_on
{𝕜 : Type u_1}
{β : Type u_4}
[linear_ordered_field 𝕜]
[linear_ordered_add_comm_monoid β]
{s : set 𝕜}
{f : 𝕜 → β}
(hs : convex 𝕜 s) :
quasilinear_on 𝕜 s f ↔ monotone_on f s ∨ antitone_on f s