English
ConcaveOn is equivalent to convexity of the domain along with a pairwise inequality for all x,y with positive coefficients, reversed.
Русский
ConcaveOn эквивалентна выпуклости области и парному неравенству с положительными коэффициентами, но в противоположном направлении.
LaTeX
$$$ConcaveOn\ 𝕜\ s\ f \iff Convex 𝕜\ s ∧ s.\text{Pairwise} (\lambda x y, ∀ a,b>0, a+b=1 \Rightarrow a f(x) + b f(y) \le f(a x + b y))$$$
Lean4
theorem concaveOn_iff_pairwise_pos {s : Set E} {f : E → β} :
ConcaveOn 𝕜 s f ↔
Convex 𝕜 s ∧
s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y) :=
convexOn_iff_pairwise_pos (β := βᵒᵈ)