mathlib3 documentation

analysis.convex.quasiconvex

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 #

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) :