convexOn_iff_slope_mono_adjacent — Mathlib

English

A function is convex on s if and only if it is convex on s and the slopes satisfy the adjacent-slope inequality for all x<y<z in s.

Русский

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

LaTeX

$$$\text{ConvexOn } 𝕜\ s\ f \;\Leftrightarrow\; \big(\text{Convex } 𝕜\ s\big) \land \forall x,y,z:\ x,z ∈ s, x

Lean4

/-- A function `f : 𝕜 → 𝕜` is convex iff for any three points `x < y < z` the slope of the secant
line of `f` on `[x, y]` is less than the slope of the secant line of `f` on `[y, z]`. -/
theorem convexOn_iff_slope_mono_adjacent :
    ConvexOn 𝕜 s f ↔
      Convex 𝕜 s ∧ ∀ ⦃x y z : 𝕜⦄, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y) :=
  ⟨fun h => ⟨h.1, fun _ _ _ => h.slope_mono_adjacent⟩, fun h =>
    convexOn_of_slope_mono_adjacent h.1 (@fun _ _ _ hx hy => h.2 hx hy)⟩

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