secant_strict_mono_aux2 — Mathlib

English

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

Lean4

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

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