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 #

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 #

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