secant_mono_aux2 — Mathlib

English

If f is convex on s, then for x<y<z with x,z ∈ s the inequality (f(y)-f(x))/(y-x) ≤ (f(z)-f(x))/(z-x) holds.

Русский

Если f выпуклая, тогда для x<y<z выполняется (f(y)-f(x))/(y-x) ≤ (f(z)-f(x))/(z-x).

LaTeX

$$$\text{ConvexOn } 𝕜\ s\ f \Rightarrow \forall x

Lean4

theorem secant_mono_aux2 (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) :
    (f y - f x) / (y - x) ≤ (f z - f x) / (z - x) :=
  by
  have hxy' : 0 < y - x := by linarith
  have hxz' : 0 < z - x := by linarith
  field_simp
  linarith only [hf.secant_mono_aux1 hx hz hxy hyz]

Похожие утверждения