secant_strict_mono_aux3 — Mathlib

English

If f is strictly convex on s, then for x<y<z 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{StrictConvexOn } 𝕜\ s\ f \Rightarrow \forall x

Lean4

theorem secant_strict_mono_aux3 (hf : StrictConvexOn 𝕜 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_strict_mono_aux1 hx hz hxy hyz]

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