Quasiconvex and quasiconcave functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

References #

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

source

def quasiconvex_on (𝕜 : Type u_1) {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [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

quasiconvex_on 𝕜 s f = ∀ (r : β), convex 𝕜 {x ∈ s | f x ≤ r}

source

def quasiconcave_on (𝕜 : Type u_1) {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [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

quasiconcave_on 𝕜 s f = ∀ (r : β), convex 𝕜 {x ∈ s | r ≤ f x}

source

def quasilinear_on (𝕜 : Type u_1) {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [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

quasilinear_on 𝕜 s f = (quasiconvex_on 𝕜 s f ∧ quasiconcave_on 𝕜 s f)

source

theorem quasiconvex_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] {s : set E} {f : E → β} :

quasiconvex_on 𝕜 s f → quasiconcave_on 𝕜 s (⇑order_dual.to_dual ∘ f)

source

theorem quasiconcave_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] {s : set E} {f : E → β} :

quasiconcave_on 𝕜 s f → quasiconvex_on 𝕜 s (⇑order_dual.to_dual ∘ f)

source

theorem quasilinear_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] {s : set E} {f : E → β} :

quasilinear_on 𝕜 s f → quasilinear_on 𝕜 s (⇑order_dual.to_dual ∘ f)

source

theorem convex.quasiconvex_on_of_convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] {s : set E} {f : E → β} (hs : convex 𝕜 s) (h : ∀ (r : β), convex 𝕜 {x : E | f x ≤ r}) :

quasiconvex_on 𝕜 s f

source

theorem convex.quasiconcave_on_of_convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] {s : set E} {f : E → β} (hs : convex 𝕜 s) (h : ∀ (r : β), convex 𝕜 {x : E | r ≤ f x}) :

quasiconcave_on 𝕜 s f

source

theorem quasiconvex_on.convex {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] {s : set E} {f : E → β} [is_directed β has_le.le] (hf : quasiconvex_on 𝕜 s f) :

convex 𝕜 s

source

theorem quasiconcave_on.convex {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] {s : set E} {f : E → β} [is_directed β ge] (hf : quasiconcave_on 𝕜 s f) :

convex 𝕜 s

source

theorem quasiconvex_on.sup {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 E] {s : set E} {f g : E → β} (hf : quasiconvex_on 𝕜 s f) (hg : quasiconvex_on 𝕜 s g) :

quasiconvex_on 𝕜 s (f ⊔ g)

source

theorem quasiconcave_on.inf {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 E] {s : set E} {f g : E → β} (hf : quasiconcave_on 𝕜 s f) (hg : quasiconcave_on 𝕜 s g) :

quasiconcave_on 𝕜 s (f ⊓ g)

source

theorem quasiconvex_on_iff_le_max {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [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)

source

theorem quasiconcave_on_iff_min_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [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)

source

theorem quasilinear_on_iff_mem_uIcc {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [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.uIcc (f x) (f y)

source

theorem quasiconvex_on.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 E] {s : set E} {f : E → β} (hf : quasiconvex_on 𝕜 s f) (r : β) :

convex 𝕜 {x ∈ s | f x < r}

source

theorem quasiconcave_on.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 E] {s : set E} {f : E → β} (hf : quasiconcave_on 𝕜 s f) (r : β) :

convex 𝕜 {x ∈ s | r < f x}

source

theorem convex_on.quasiconvex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) :

quasiconvex_on 𝕜 s f

source

theorem concave_on.quasiconcave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) :

quasiconcave_on 𝕜 s f

source

theorem monotone_on.quasiconvex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E → β} (hf : monotone_on f s) (hs : convex 𝕜 s) :

quasiconvex_on 𝕜 s f

source

theorem monotone_on.quasiconcave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E → β} (hf : monotone_on f s) (hs : convex 𝕜 s) :

quasiconcave_on 𝕜 s f

source

theorem monotone_on.quasilinear_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E → β} (hf : monotone_on f s) (hs : convex 𝕜 s) :

quasilinear_on 𝕜 s f

source

theorem antitone_on.quasiconvex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E → β} (hf : antitone_on f s) (hs : convex 𝕜 s) :

quasiconvex_on 𝕜 s f

source

theorem antitone_on.quasiconcave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E → β} (hf : antitone_on f s) (hs : convex 𝕜 s) :

quasiconcave_on 𝕜 s f

source

theorem antitone_on.quasilinear_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} {f : E → β} (hf : antitone_on f s) (hs : convex 𝕜 s) :

quasilinear_on 𝕜 s f

source

theorem monotone.quasiconvex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E → β} (hf : monotone f) :

quasiconvex_on 𝕜 set.univ f

source

theorem monotone.quasiconcave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E → β} (hf : monotone f) :

quasiconcave_on 𝕜 set.univ f

source

theorem monotone.quasilinear_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E → β} (hf : monotone f) :

quasilinear_on 𝕜 set.univ f

source

theorem antitone.quasiconvex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E → β} (hf : antitone f) :

quasiconvex_on 𝕜 set.univ f

source

theorem antitone.quasiconcave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E → β} (hf : antitone f) :

quasiconcave_on 𝕜 set.univ f

source

theorem antitone.quasilinear_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [ordered_smul 𝕜 E] {f : E → β} (hf : antitone f) :

quasilinear_on 𝕜 set.univ f

source

theorem quasilinear_on.monotone_on_or_antitone_on {𝕜 : Type u_1} {β : Type u_4} [linear_ordered_field 𝕜] [linear_ordered_add_comm_monoid β] {s : set 𝕜} {f : 𝕜 → β} (hf : quasilinear_on 𝕜 s f) :

monotone_on f s ∨ antitone_on f s

source

theorem quasilinear_on_iff_monotone_on_or_antitone_on {𝕜 : Type u_1} {β : Type u_4} [linear_ordered_field 𝕜] [linear_ordered_add_comm_monoid β] {s : set 𝕜} {f : 𝕜 → β} (hs : convex 𝕜 s) :

quasilinear_on 𝕜 s f ↔ monotone_on f s ∨ antitone_on f s