quasiconcaveOn — Mathlib

English

QuasiconcaveOn 𝕜 s f is equivalent to convexity of s together with the inequality using max of f at the endpoints.

Русский

Квазиконкавность On 𝕜 s f эквивалентна выпуклости s и неравенству с max(f(x), f(y)).

LaTeX

$$$QuasiconcaveOn\ 𝕜\ s\ f \iff Convex\ 𝕜\ s \land \forall\{x\}, x\in s \to \forall\{y\}, y\in s \to \forall\{a,b\}: 𝕜, 0\le a \to 0\le b \to a+b=1 \to f(a\cdot x+b\cdot y) \le \max(f(x),f(y))$$$

Lean4

theorem quasiconcaveOn (hf : AntitoneOn f s) (hs : Convex 𝕜 s) : QuasiconcaveOn 𝕜 s f :=
  hf.convex_ge hs

Похожие утверждения