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

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}

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}

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)

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)

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)

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)

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

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

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

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

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)

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)

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

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)

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)

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}

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}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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