English
Convex on s is equivalent to convexity of s plus a pairwise inequality for all distinct x,y in s with positive coefficients.
Русский
ConvexOn эквивалентна выпуклости s и парному неравенству для всех различных x,y в s с положительными коэффициентами.
LaTeX
$$$ConvexOn\ 𝕜\ s\ f \iff Convex 𝕜\ s ∧ s.\text{Pairwise} (\lambda x y, ∀ a,b>0, a+b=1 \Rightarrow f(a x + b y) \le a f(x) + b f(y))$$$
Lean4
theorem convexOn_iff_pairwise_pos {s : Set E} {f : E → β} :
ConvexOn 𝕜 s f ↔
Convex 𝕜 s ∧
s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y :=
by
rw [convexOn_iff_forall_pos]
refine and_congr_right' ⟨fun h x hx y hy _ a b ha hb hab => h hx hy ha hb hab, fun h x hx y hy a b ha hb hab => ?_⟩
obtain rfl | hxy := eq_or_ne x y
· rw [Convex.combo_self hab, Convex.combo_self hab]
exact h hx hy hxy ha hb hab
