strictConcaveOn_iff_slope_strict_anti_adjacent

English

A function is strictly convex on s iff it is convex on s and the slope inequality is strict for all x<y<z in s.

Русский

Функция строго выпукла на s тогда и только тогда, когда она выпукла на s и наклонное неравенство строго для всех x<y<z.

LaTeX

$$$\text{StrictConvexOn } 𝕜\ s\ f \iff \Big(\text{ConvexOn } 𝕜\ s\ f \land \forall x,y,z:\ x∈s, z∈s, x

Lean4

/-- A function `f : 𝕜 → 𝕜` is strictly concave iff 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 strictConcaveOn_iff_slope_strict_anti_adjacent :
    StrictConcaveOn 𝕜 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 =>
    strictConcaveOn_of_slope_strict_anti_adjacent h.1 (@fun _ _ _ hx hy => h.2 hx hy)⟩

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