English
If f is strictly 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
$$$\forall a,x,y:\ a\in s, x\in s, y\in s, a\neq x, y\neq a, x\le y \Rightarrow \frac{f(x)-f(a)}{x-a} \le \frac{f(y)-f(a)}{y-a}. $$$
Lean4
/-- If `f : 𝕜 → 𝕜` is strictly convex, then for any point `a` the slope of the secant line of `f`
through `a` and `b` is strictly monotone with respect to `b`. -/
theorem secant_strict_mono (hf : StrictConvexOn 𝕜 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 lt_or_gt_of_ne hxa with hxa | hxa
· rcases lt_or_gt_of_ne hya with hya | hya
· convert hf.secant_strict_mono_aux3 hx ha hxy hya using 1 <;> rw [← neg_div_neg_eq] <;> simp
· convert hf.slope_strict_mono_adjacent hx hy hxa hya using 1
rw [← neg_div_neg_eq]; simp
· exact hf.secant_strict_mono_aux2 ha hy hxa hxy
