slope_anti_adjacent — Mathlib

English

Let f be concave on a set s. For any x < y < z with x, z in s, the slope of the secant line on [y, z] is no greater than the slope on [x, y]. In particular, the secant slopes decrease as you move to the right.

Русский

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

LaTeX

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

Lean4

/-- If `f : 𝕜 → 𝕜` is concave, then for any three points `x < y < z` the slope of the secant line of
`f` on `[x, y]` is greater than the slope of the secant line of `f` on `[y, z]`. -/
theorem slope_anti_adjacent (hf : ConcaveOn 𝕜 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 := ConvexOn.slope_mono_adjacent hf.neg hx hz hxy hyz
  simp only [Pi.neg_apply] at this
  linear_combination this

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