slope_anti_adjacent — Mathlib

English

If f is strictly concave on s, then for any x < y < z with x, z ∈ s, the slope on [y, z] is strictly less than the slope on [x, y].

Русский

Пусть f строго вогнута на s. Тогда для любых x < y < z с x, z ∈ s наклон секущей на [y, z] строго меньше наклона на [x, y].

LaTeX

$$$\text{StrictConcaveOn } 𝕜\ s\ f \Rightarrow \forall x,y,z\in 𝕜,\ x∈s,\ z∈s,\ x

Lean4

/-- If `f : 𝕜 → 𝕜` is strictly concave, then for any three points `x < y < z` the slope of the
secant line of `f` on `[x, y]` is strictly greater than the slope of the secant line of `f` on
`[y, z]`. -/
theorem slope_anti_adjacent (hf : StrictConcaveOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y)
    (hyz : y < z) : (f z - f y) / (z - y) < (f y - f x) / (y - x) :=
  by
  have := StrictConvexOn.slope_strict_mono_adjacent hf.neg hx hz hxy hyz
  simp only [Pi.neg_apply] at this
  linear_combination this

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