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.
TODO #
Prove that a quasilinear function between two linear orders is either monotone or antitone. This is not hard but quite a pain to go about as there are many cases to consider.
References #
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}
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}
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)