secant_mono_aux3 — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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