# mathlibdocumentation

analysis.convex.quasiconvex

# 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 function f on the set s with scalars π. This means that, for all r, {x β s | f x β€ r} is π-convex.
• quasiconcave_on π s f: Quasiconcavity of the function f on the set s with scalars π. This means that, for all r, {x β s | r β€ f x} is π-convex.
• quasilinear_on π s f: Quasilinearity of the function f on the set s with scalars π. This means that f 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 #

def quasiconvex_on (π : Type u_1) {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [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
def quasiconcave_on (π : Type u_1) {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [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
def quasilinear_on (π : Type u_1) {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [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
theorem quasiconvex_on.dual {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [has_smul π E] {s : set E} {f : E β Ξ²} :
quasiconvex_on π s f β quasiconcave_on π s
theorem quasiconcave_on.dual {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [has_smul π E] {s : set E} {f : E β Ξ²} :
quasiconcave_on π s f β quasiconvex_on π s
theorem quasilinear_on.dual {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [has_smul π E] {s : set E} {f : E β Ξ²} :
quasilinear_on π s f β quasilinear_on π s
theorem convex.quasiconvex_on_of_convex_le {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [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 π] [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 π] [has_smul π E] {s : set E} {f : E β Ξ²} [ 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 π] [has_smul π E] {s : set E} {f : E β Ξ²} [ ge] (hf : quasiconcave_on π s f) :
convex π s
theorem quasiconvex_on.sup {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [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 π] [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 π] [has_smul π E] {s : set E} {f : E β Ξ²} :
quasiconvex_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) β€ linear_order.max (f x) (f y)
theorem quasiconcave_on_iff_min_le {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [has_smul π E] {s : set E} {f : E β Ξ²} :
quasiconcave_on π s f β convex π s β§ β β¦x : Eβ¦, x β s β β β¦y : Eβ¦, y β s β β β¦a b : πβ¦, 0 β€ a β 0 β€ b β a + b = 1 β linear_order.min (f x) (f y) β€ f (a β’ x + b β’ y)
theorem quasilinear_on_iff_mem_interval {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [has_smul π E] {s : set E} {f : E β Ξ²} :
quasilinear_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) β set.interval (f x) (f y)
theorem quasiconvex_on.convex_lt {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [has_smul π E] {s : set E} {f : E β Ξ²} (hf : quasiconvex_on π s f) (r : Ξ²) :
convex π {x β s | f x < r}
theorem quasiconcave_on.convex_gt {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [has_smul π E] {s : set E} {f : E β Ξ²} (hf : quasiconcave_on π s f) (r : Ξ²) :
convex π {x β s | r < f x}
theorem convex_on.quasiconvex_on {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [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 π] [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 π] [module π E] [ordered_smul π E] {s : set E} {f : E β Ξ²} (hf : 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 π] [module π E] [ordered_smul π E] {s : set E} {f : E β Ξ²} (hf : 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 π] [module π E] [ordered_smul π E] {s : set E} {f : E β Ξ²} (hf : 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 π] [module π E] [ordered_smul π E] {s : set E} {f : E β Ξ²} (hf : 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 π] [module π E] [ordered_smul π E] {s : set E} {f : E β Ξ²} (hf : 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 π] [module π E] [ordered_smul π E] {s : set E} {f : E β Ξ²} (hf : s) (hs : convex π s) :
quasilinear_on π s f
theorem monotone.quasiconvex_on {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [module π E] [ordered_smul π E] {f : E β Ξ²} (hf : monotone f) :
f
theorem monotone.quasiconcave_on {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [module π E] [ordered_smul π E] {f : E β Ξ²} (hf : monotone f) :
f
theorem monotone.quasilinear_on {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [module π E] [ordered_smul π E] {f : E β Ξ²} (hf : monotone f) :
f
theorem antitone.quasiconvex_on {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [module π E] [ordered_smul π E] {f : E β Ξ²} (hf : antitone f) :
f
theorem antitone.quasiconcave_on {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [module π E] [ordered_smul π E] {f : E β Ξ²} (hf : antitone f) :
f
theorem antitone.quasilinear_on {π : Type u_1} {E : Type u_2} {Ξ² : Type u_4} [ordered_semiring π] [module π E] [ordered_smul π E] {f : E β Ξ²} (hf : antitone f) :
f