secant_strict_mono — 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

/-- If `f : 𝕜 → 𝕜` is strictly concave, then for any point `a` the slope of the secant line of `f`
through `a` and `b` is strictly antitone with respect to `b`. -/
theorem secant_strict_mono (hf : StrictConcaveOn 𝕜 s f) {a x y : 𝕜} (ha : a ∈ s) (hx : x ∈ s) (hy : y ∈ s) (hxa : x ≠ a)
    (hya : y ≠ a) (hxy : x < y) : (f y - f a) / (y - a) < (f x - f a) / (x - a) :=
  by
  have key := hf.neg.secant_strict_mono ha hx hy hxa hya hxy
  simp only [Pi.neg_apply] at key
  linear_combination key

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