mathlib documentation

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 #

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

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}

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}

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)

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)

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)

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)

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

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

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

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

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)

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)

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)

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)

theorem quasilinear_on_iff_mem_interval {𝕜 : 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.interval (f x) (f y)

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}

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}

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

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

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

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

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

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

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

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

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

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

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

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

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

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