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 #

https://en.wikipedia.org/wiki/Quasiconvex_function

source

def QuasiconvexOn (𝕜 : Type u_1) {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [LE β] [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

QuasiconvexOn 𝕜 s f = ∀ (r : β), Convex 𝕜 {x : E | x ∈ s ∧ f x ≤ r}

Instances For

source

def QuasiconcaveOn (𝕜 : Type u_1) {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [LE β] [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

QuasiconcaveOn 𝕜 s f = ∀ (r : β), Convex 𝕜 {x : E | x ∈ s ∧ r ≤ f x}

Instances For

source

def QuasilinearOn (𝕜 : Type u_1) {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [LE β] [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

QuasilinearOn 𝕜 s f = (QuasiconvexOn 𝕜 s f ∧ QuasiconcaveOn 𝕜 s f)

Instances For

source

theorem QuasiconvexOn.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [LE β] [SMul 𝕜 E] {s : Set E} {f : E → β} :

QuasiconvexOn 𝕜 s f → QuasiconcaveOn 𝕜 s (⇑OrderDual.toDual ∘ f)

source

theorem QuasiconcaveOn.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [LE β] [SMul 𝕜 E] {s : Set E} {f : E → β} :

QuasiconcaveOn 𝕜 s f → QuasiconvexOn 𝕜 s (⇑OrderDual.toDual ∘ f)

source

theorem QuasilinearOn.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [LE β] [SMul 𝕜 E] {s : Set E} {f : E → β} :

QuasilinearOn 𝕜 s f → QuasilinearOn 𝕜 s (⇑OrderDual.toDual ∘ f)

source

theorem Convex.quasiconvexOn_of_convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [LE β] [SMul 𝕜 E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s) (h : ∀ (r : β), Convex 𝕜 {x : E | f x ≤ r}) :

QuasiconvexOn 𝕜 s f

source

theorem Convex.quasiconcaveOn_of_convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [LE β] [SMul 𝕜 E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s) (h : ∀ (r : β), Convex 𝕜 {x : E | r ≤ f x}) :

QuasiconcaveOn 𝕜 s f

source

theorem QuasiconvexOn.convex {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [LE β] [SMul 𝕜 E] {s : Set E} {f : E → β} [IsDirected β fun (x1 x2 : β) => x1 ≤ x2] (hf : QuasiconvexOn 𝕜 s f) :

Convex 𝕜 s

source

theorem QuasiconcaveOn.convex {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [LE β] [SMul 𝕜 E] {s : Set E} {f : E → β} [IsDirected β fun (x1 x2 : β) => x1 ≥ x2] (hf : QuasiconcaveOn 𝕜 s f) :

Convex 𝕜 s

source

theorem QuasiconvexOn.sup {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} {f g : E → β} [SemilatticeSup β] (hf : QuasiconvexOn 𝕜 s f) (hg : QuasiconvexOn 𝕜 s g) :

QuasiconvexOn 𝕜 s (f ⊔ g)

source

theorem QuasiconcaveOn.inf {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {s : Set E} {f g : E → β} [SemilatticeInf β] (hf : QuasiconcaveOn 𝕜 s f) (hg : QuasiconcaveOn 𝕜 s g) :

QuasiconcaveOn 𝕜 s (f ⊓ g)

source

theorem quasiconvexOn_iff_le_max {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrder β] [SMul 𝕜 E] {s : Set E} {f : E → β} :

QuasiconvexOn 𝕜 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) ≤ f x ⊔ f y

source

theorem quasiconcaveOn_iff_min_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrder β] [SMul 𝕜 E] {s : Set E} {f : E → β} :

QuasiconcaveOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f x ⊓ f y ≤ f (a • x + b • y)

source

theorem quasilinearOn_iff_mem_uIcc {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrder β] [SMul 𝕜 E] {s : Set E} {f : E → β} :

QuasilinearOn 𝕜 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.uIcc (f x) (f y)

source

theorem QuasiconvexOn.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrder β] [SMul 𝕜 E] {s : Set E} {f : E → β} (hf : QuasiconvexOn 𝕜 s f) (r : β) :

Convex 𝕜 {x : E | x ∈ s ∧ f x < r}

source

theorem QuasiconcaveOn.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [LinearOrder β] [SMul 𝕜 E] {s : Set E} {f : E → β} (hf : QuasiconcaveOn 𝕜 s f) (r : β) :

Convex 𝕜 {x : E | x ∈ s ∧ r < f x}

source

theorem ConvexOn.quasiconvexOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConvexOn 𝕜 s f) :

QuasiconvexOn 𝕜 s f

source

theorem ConcaveOn.quasiconcaveOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β} (hf : ConcaveOn 𝕜 s f) :

QuasiconcaveOn 𝕜 s f

source

theorem MonotoneOn.quasiconvexOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) :

QuasiconvexOn 𝕜 s f

source

theorem MonotoneOn.quasiconcaveOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) :

QuasiconcaveOn 𝕜 s f

source

theorem MonotoneOn.quasilinearOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {s : Set E} {f : E → β} (hf : MonotoneOn f s) (hs : Convex 𝕜 s) :

QuasilinearOn 𝕜 s f

source

theorem AntitoneOn.quasiconvexOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {s : Set E} {f : E → β} (hf : AntitoneOn f s) (hs : Convex 𝕜 s) :

QuasiconvexOn 𝕜 s f

source

theorem AntitoneOn.quasiconcaveOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {s : Set E} {f : E → β} (hf : AntitoneOn f s) (hs : Convex 𝕜 s) :

QuasiconcaveOn 𝕜 s f

source

theorem AntitoneOn.quasilinearOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {s : Set E} {f : E → β} (hf : AntitoneOn f s) (hs : Convex 𝕜 s) :

QuasilinearOn 𝕜 s f

source

theorem Monotone.quasiconvexOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {f : E → β} (hf : Monotone f) :

QuasiconvexOn 𝕜 Set.univ f

source

theorem Monotone.quasiconcaveOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {f : E → β} (hf : Monotone f) :

QuasiconcaveOn 𝕜 Set.univ f

source

theorem Monotone.quasilinearOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {f : E → β} (hf : Monotone f) :

QuasilinearOn 𝕜 Set.univ f

source

theorem Antitone.quasiconvexOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {f : E → β} (hf : Antitone f) :

QuasiconvexOn 𝕜 Set.univ f

source

theorem Antitone.quasiconcaveOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {f : E → β} (hf : Antitone f) :

QuasiconcaveOn 𝕜 Set.univ f

source

theorem Antitone.quasilinearOn {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid E] [OrderedAddCommMonoid β] [Module 𝕜 E] [OrderedSMul 𝕜 E] {f : E → β} (hf : Antitone f) :

QuasilinearOn 𝕜 Set.univ f

source

theorem QuasilinearOn.monotoneOn_or_antitoneOn {𝕜 : Type u_1} {β : Type u_3} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → β} [LinearOrder β] (hf : QuasilinearOn 𝕜 s f) :

MonotoneOn f s ∨ AntitoneOn f s

source

theorem quasilinearOn_iff_monotoneOn_or_antitoneOn {𝕜 : Type u_1} {β : Type u_3} [LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → β} [LinearOrderedAddCommMonoid β] (hs : Convex 𝕜 s) :

QuasilinearOn 𝕜 s f ↔ MonotoneOn f s ∨ AntitoneOn f s

Documentation

Mathlib.Analysis.Convex.Quasiconvex

Quasiconvex and quasiconcave functions #

Main declarations #

References #