strictConcaveOn_of_slope_strict_anti_adjacent

English

If for any x<y<z the slope of the secant line on [x,y] is strictly greater than the slope on [y,z], then f is strictly concave on s.

Русский

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

LaTeX

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

Lean4

/-- If 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]`, then `f` is strictly concave.
-/
theorem strictConcaveOn_of_slope_strict_anti_adjacent (hs : Convex 𝕜 s)
    (hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)) :
    StrictConcaveOn 𝕜 s f := by
  rw [← neg_strictConvexOn_iff]
  refine strictConvexOn_of_slope_strict_mono_adjacent hs fun hx hz hxy hyz => ?_
  simp only [Pi.neg_apply]
  linear_combination hf hx hz hxy hyz

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