English
If f is convex on s, then for any a, x, y with a, x, y ∈ s and a ≠ x, a ≠ y and x ≤ y, the secant slopes satisfy
Русский
Если f выпуклая на s, тогда для a, x, y ∈ s с a ≠ x, a ≠ y и x ≤ y выполняется неравенство наклонов секущих:
LaTeX
$$$\text{ConvexOn } 𝕜\ s\ f \Rightarrow \forall a,x,y:\ a\in s, x\in s, y\in s, a\neq x, y\neq a, x\le y:\ \frac{f(x)-f(a)}{x-a} \le \frac{f(y)-f(a)}{y-a}. $$$
Lean4
/-- If `f : 𝕜 → 𝕜` is convex, then for any point `a` the slope of the secant line of `f` through `a`
and `b ≠ a` is monotone with respect to `b`. -/
theorem secant_mono (hf : ConvexOn 𝕜 s f) {a x y : 𝕜} (ha : a ∈ s) (hx : x ∈ s) (hy : y ∈ s) (hxa : x ≠ a) (hya : y ≠ a)
(hxy : x ≤ y) : (f x - f a) / (x - a) ≤ (f y - f a) / (y - a) :=
by
rcases eq_or_lt_of_le hxy with (rfl | hxy)
· simp
rcases lt_or_gt_of_ne hxa with hxa | hxa
· rcases lt_or_gt_of_ne hya with hya | hya
· convert hf.secant_mono_aux3 hx ha hxy hya using 1 <;> rw [← neg_div_neg_eq] <;> simp
· convert hf.slope_mono_adjacent hx hy hxa hya using 1
rw [← neg_div_neg_eq]; simp
· exact hf.secant_mono_aux2 ha hy hxa hxy
