concaveOn_iff_slope_anti_adjacent

English

If for all x<y<z the slope on [z,y] is not greater than the slope on [y,x], then f is concave on s.

Русский

Если для всех x<y<z уклон на [z,y] не превышает уклона на [y,x], то f выпукла на s.

LaTeX

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

Lean4

/-- A function `f : 𝕜 → 𝕜` is concave iff 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 concaveOn_iff_slope_anti_adjacent :
    ConcaveOn 𝕜 s f ↔
      Convex 𝕜 s ∧ ∀ ⦃x y z : 𝕜⦄, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x) :=
  ⟨fun h => ⟨h.1, fun _ _ _ => h.slope_anti_adjacent⟩, fun h =>
    concaveOn_of_slope_anti_adjacent h.1 (@fun _ _ _ hx hy => h.2 hx hy)⟩

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