concaveOn_of_slope_anti_adjacent — Mathlib

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\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
greater than the slope of the secant line of `f` on `[y, z]`, then `f` is concave. -/
theorem concaveOn_of_slope_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)) :
    ConcaveOn 𝕜 s f := by
  rw [← neg_convexOn_iff]
  refine convexOn_of_slope_mono_adjacent hs fun hx hz hxy hyz => ?_
  simp only [Pi.neg_apply]
  linear_combination hf hx hz hxy hyz

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