# 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 #

• QuasiconvexOn 𝕜 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.
• QuasiconcaveOn 𝕜 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.
• QuasilinearOn 𝕜 s f: Quasilinearity of the function f on the set s with scalars 𝕜. This means that f is both quasiconvex and quasiconcave.

## References #

def QuasiconvexOn (𝕜 : Type u_1) {E : Type u_2} {β : Type u_4} [] [] [LE β] [SMul 𝕜 E] (s : Set E) (f : Eβ) :

A function is quasiconvex if all its sublevels are convex. This means that, for all r, {x ∈ s | f x ≤ r} is 𝕜-convex.

Equations
Instances For
def QuasiconcaveOn (𝕜 : Type u_1) {E : Type u_2} {β : Type u_4} [] [] [LE β] [SMul 𝕜 E] (s : Set E) (f : Eβ) :

A function is quasiconcave if all its superlevels are convex. This means that, for all r, {x ∈ s | r ≤ f x} is 𝕜-convex.

Equations
Instances For
def QuasilinearOn (𝕜 : Type u_1) {E : Type u_2} {β : Type u_4} [] [] [LE β] [SMul 𝕜 E] (s : Set E) (f : Eβ) :

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
Instances For
theorem QuasiconvexOn.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [] [LE β] [SMul 𝕜 E] {s : Set E} {f : Eβ} :
QuasiconcaveOn 𝕜 s (OrderDual.toDual f)
theorem QuasiconcaveOn.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [] [LE β] [SMul 𝕜 E] {s : Set E} {f : Eβ} :
QuasiconvexOn 𝕜 s (OrderDual.toDual f)
theorem QuasilinearOn.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [] [LE β] [SMul 𝕜 E] {s : Set E} {f : Eβ} :
QuasilinearOn 𝕜 s (OrderDual.toDual f)
theorem Convex.quasiconvexOn_of_convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [] [LE β] [SMul 𝕜 E] {s : Set E} {f : Eβ} (hs : Convex 𝕜 s) (h : ∀ (r : β), Convex 𝕜 {x : E | f x r}) :
theorem Convex.quasiconcaveOn_of_convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [] [LE β] [SMul 𝕜 E] {s : Set E} {f : Eβ} (hs : Convex 𝕜 s) (h : ∀ (r : β), Convex 𝕜 {x : E | r f x}) :
theorem QuasiconvexOn.convex {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [] [LE β] [SMul 𝕜 E] {s : Set E} {f : Eβ} [IsDirected β fun (x1 x2 : β) => x1 x2] (hf : ) :
Convex 𝕜 s
theorem QuasiconcaveOn.convex {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [] [LE β] [SMul 𝕜 E] {s : Set E} {f : Eβ} [IsDirected β fun (x1 x2 : β) => x1 x2] (hf : ) :
Convex 𝕜 s
theorem QuasiconvexOn.sup {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [] [SMul 𝕜 E] {s : Set E} {f : Eβ} {g : Eβ} [] (hf : ) (hg : ) :
QuasiconvexOn 𝕜 s (f g)
theorem QuasiconcaveOn.inf {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [] [SMul 𝕜 E] {s : Set E} {f : Eβ} {g : Eβ} [] (hf : ) (hg : ) :
QuasiconcaveOn 𝕜 s (f g)
theorem quasiconvexOn_iff_le_max {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [] [] [SMul 𝕜 E] {s : Set E} {f : Eβ} :
Convex 𝕜 s ∀ ⦃x : E⦄, x s∀ ⦃y : E⦄, y s∀ ⦃a b : 𝕜⦄, 0 a0 ba + b = 1f (a x + b y) max (f x) (f y)
theorem quasiconcaveOn_iff_min_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [] [] [SMul 𝕜 E] {s : Set E} {f : Eβ} :
Convex 𝕜 s ∀ ⦃x : E⦄, x s∀ ⦃y : E⦄, y s∀ ⦃a b : 𝕜⦄, 0 a0 ba + b = 1min (f x) (f y) f (a x + b y)
theorem quasilinearOn_iff_mem_uIcc {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [] [] [SMul 𝕜 E] {s : Set E} {f : Eβ} :
Convex 𝕜 s ∀ ⦃x : E⦄, x s∀ ⦃y : E⦄, y s∀ ⦃a b : 𝕜⦄, 0 a0 ba + b = 1f (a x + b y) Set.uIcc (f x) (f y)
theorem QuasiconvexOn.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [] [] [SMul 𝕜 E] {s : Set E} {f : Eβ} (hf : ) (r : β) :
Convex 𝕜 {x : E | x s f x < r}
theorem QuasiconcaveOn.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [] [] [SMul 𝕜 E] {s : Set E} {f : Eβ} (hf : ) (r : β) :
Convex 𝕜 {x : E | x s r < f x}
theorem ConvexOn.quasiconvexOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [] [Module 𝕜 E] [Module 𝕜 β] [] {s : Set E} {f : Eβ} (hf : ConvexOn 𝕜 s f) :
theorem ConcaveOn.quasiconcaveOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [] [Module 𝕜 E] [Module 𝕜 β] [] {s : Set E} {f : Eβ} (hf : ConcaveOn 𝕜 s f) :
theorem MonotoneOn.quasiconvexOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [Module 𝕜 E] [] {s : Set E} {f : Eβ} (hf : ) (hs : Convex 𝕜 s) :
theorem MonotoneOn.quasiconcaveOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [Module 𝕜 E] [] {s : Set E} {f : Eβ} (hf : ) (hs : Convex 𝕜 s) :
theorem MonotoneOn.quasilinearOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [Module 𝕜 E] [] {s : Set E} {f : Eβ} (hf : ) (hs : Convex 𝕜 s) :
theorem AntitoneOn.quasiconvexOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [Module 𝕜 E] [] {s : Set E} {f : Eβ} (hf : ) (hs : Convex 𝕜 s) :
theorem AntitoneOn.quasiconcaveOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [Module 𝕜 E] [] {s : Set E} {f : Eβ} (hf : ) (hs : Convex 𝕜 s) :
theorem AntitoneOn.quasilinearOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [Module 𝕜 E] [] {s : Set E} {f : Eβ} (hf : ) (hs : Convex 𝕜 s) :
theorem Monotone.quasiconvexOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [Module 𝕜 E] [] {f : Eβ} (hf : ) :
QuasiconvexOn 𝕜 Set.univ f
theorem Monotone.quasiconcaveOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [Module 𝕜 E] [] {f : Eβ} (hf : ) :
QuasiconcaveOn 𝕜 Set.univ f
theorem Monotone.quasilinearOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [Module 𝕜 E] [] {f : Eβ} (hf : ) :
QuasilinearOn 𝕜 Set.univ f
theorem Antitone.quasiconvexOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [Module 𝕜 E] [] {f : Eβ} (hf : ) :
QuasiconvexOn 𝕜 Set.univ f
theorem Antitone.quasiconcaveOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [Module 𝕜 E] [] {f : Eβ} (hf : ) :
QuasiconcaveOn 𝕜 Set.univ f
theorem Antitone.quasilinearOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [] [Module 𝕜 E] [] {f : Eβ} (hf : ) :
QuasilinearOn 𝕜 Set.univ f
theorem QuasilinearOn.monotoneOn_or_antitoneOn {𝕜 : Type u_1} {β : Type u_4} {s : Set 𝕜} {f : 𝕜β} [] (hf : ) :
theorem quasilinearOn_iff_monotoneOn_or_antitoneOn {𝕜 : Type u_1} {β : Type u_4} {s : Set 𝕜} {f : 𝕜β} (hs : Convex 𝕜 s) :