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 #

References #

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
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
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
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 β} :
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 β} :
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 β} :
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}) :
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}) :
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_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)
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :