Commit 2021-10-09 07:26 e0f80e78

View on Github →

feat(analysis/convex/quasiconvex): Quasiconvexity of functions (#9561) A function is quasiconvex iff all its sublevels are convex. This generalizes unimodality to non-ordered spaces.

Estimated changes

Created src/analysis/convex/quasiconvex.lean

added theorem antitone.quasiconcave_on

added theorem antitone.quasiconvex_on

added theorem antitone.quasilinear_on

added theorem antitone_on.quasiconcave_on

added theorem antitone_on.quasiconvex_on

added theorem antitone_on.quasilinear_on

added theorem concave_on.quasiconcave_on

added theorem convex.quasiconcave_on_of_convex_ge

added theorem convex.quasiconvex_on_of_convex_le

added theorem convex_on.quasiconvex_on

added theorem monotone.quasiconcave_on

added theorem monotone.quasiconvex_on

added theorem monotone.quasilinear_on

added theorem monotone_on.quasiconcave_on

added theorem monotone_on.quasiconvex_on

added theorem monotone_on.quasilinear_on

added theorem quasiconcave_on.convex

added theorem quasiconcave_on.convex_gt

added theorem quasiconcave_on.dual

added theorem quasiconcave_on.inf

added def quasiconcave_on

added theorem quasiconcave_on_iff_min_le

added theorem quasiconvex_on.convex

added theorem quasiconvex_on.convex_lt

added theorem quasiconvex_on.dual

added theorem quasiconvex_on.sup

added def quasiconvex_on

added theorem quasiconvex_on_iff_le_max

added theorem quasilinear_on.dual

added def quasilinear_on

added theorem quasilinear_on_iff_mem_interval

Modified src/data/set/basic.lean

added theorem set.sep_inter_sep