English
On a linearly ordered space, to prove convexity it suffices to verify the midpoint inequality when x < y and a,b > 0 with a+b=1.
Русский
На линейно упорядоченном пространстве достаточно проверить неравенство на миля между точками x<y при положительных a,b с a+b=1, чтобы доказать выпуклость.
LaTeX
$$$\forall x,y\in s,\; x0,\; a+b=1:\ f(a x + b y) \le a f(x) + b f(y)$ ⇒ $\forall x,y\in s:\ ConvexOn 𝕜 s f$$$
Lean4
/-- For a function on a convex set in a linearly ordered space (where the order and the algebraic
structures aren't necessarily compatible), in order to prove that it is convex, it suffices to
verify the inequality `f (a • x + b • y) ≤ a • f x + b • f y` only for `x < y` and positive `a`,
`b`. The main use case is `E = 𝕜` however one can apply it, e.g., to `𝕜^n` with lexicographic order.
-/
theorem convexOn_of_lt (hs : Convex 𝕜 s)
(hf :
∀ ⦃x⦄,
x ∈ s → ∀ ⦃y⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y) :
ConvexOn 𝕜 s f :=
by
refine convexOn_iff_pairwise_pos.2 ⟨hs, fun x hx y hy hxy a b ha hb hab => ?_⟩
wlog h : x < y
· rw [add_comm (a • x), add_comm (a • f x)]
rw [add_comm] at hab
exact this hs hf y hy x hx hxy.symm b a hb ha hab (hxy.lt_or_gt.resolve_left h)
exact hf hx hy h ha hb hab
