English
Characterization: convexOn is equivalent to convexity of the domain and the usual positive-scalar inequality for all positive coefficients.
Русский
Характеризация: выпуклость эквивалентна выпуклости области и обычному неравенству для всех положительных коэффициентов.
LaTeX
$$$ConvexOn\ 𝕜\ s\ f \iff (Convex\ 𝕜\ s \land \forall x\in s\forall y\in s\forall a,b>0, a+b=1 \Rightarrow f(a x + b y) \le a f(x) + b f(y))$$$
Lean4
theorem convexOn_iff_forall_pos {s : Set E} {f : E → β} :
ConvexOn 𝕜 s f ↔
Convex 𝕜 s ∧
∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y :=
by
refine
and_congr_right' ⟨fun h x hx y hy a b ha hb hab => h hx hy ha.le hb.le hab, fun h x hx y hy a b ha hb hab => ?_⟩
obtain rfl | ha' := ha.eq_or_lt
· rw [zero_add] at hab
subst b
simp_rw [zero_smul, zero_add, one_smul, le_rfl]
obtain rfl | hb' := hb.eq_or_lt
· rw [add_zero] at hab
subst a
simp_rw [zero_smul, add_zero, one_smul, le_rfl]
exact h hx hy ha' hb' hab
