Commit 2023-04-12 19:26 22a23994

View on Github →

feat: port Analysis.Convex.Quasiconvex (#3412)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Quasiconvex.lean

added theorem Antitone.quasiconcaveOn

added theorem Antitone.quasiconvexOn

added theorem Antitone.quasilinearOn

added theorem AntitoneOn.quasiconcaveOn

added theorem AntitoneOn.quasiconvexOn

added theorem AntitoneOn.quasilinearOn

added theorem ConcaveOn.quasiconcaveOn

added theorem Convex.quasiconcaveOn_of_convex_ge

added theorem Convex.quasiconvexOn_of_convex_le

added theorem ConvexOn.quasiconvexOn

added theorem Monotone.quasiconcaveOn

added theorem Monotone.quasiconvexOn

added theorem Monotone.quasilinearOn

added theorem MonotoneOn.quasiconcaveOn

added theorem MonotoneOn.quasiconvexOn

added theorem MonotoneOn.quasilinearOn

added theorem QuasiconcaveOn.convex

added theorem QuasiconcaveOn.convex_gt

added theorem QuasiconcaveOn.dual

added theorem QuasiconcaveOn.inf

added def QuasiconcaveOn

added theorem QuasiconvexOn.convex

added theorem QuasiconvexOn.convex_lt

added theorem QuasiconvexOn.dual

added theorem QuasiconvexOn.sup

added def QuasiconvexOn

added theorem QuasilinearOn.dual

added theorem QuasilinearOn.monotoneOn_or_antitoneOn

added def QuasilinearOn

added theorem quasiconcaveOn_iff_min_le

added theorem quasiconvexOn_iff_le_max

added theorem quasilinearOn_iff_mem_uIcc

added theorem quasilinearOn_iff_monotoneOn_or_antitoneOn