convexOn_of_slope_mono_adjacent — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If 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]`, then `f` is convex. -/
theorem convexOn_of_slope_mono_adjacent (hs : Convex 𝕜 s)
    (hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)) :
    ConvexOn 𝕜 s f :=
  LinearOrder.convexOn_of_lt hs fun x hx z hz hxz a b ha hb hab =>
    by
    simp only [smul_eq_mul]
    have hxy : x < a * x + b * z := by linear_combination b * hxz - x * hab
    have hyz : a * x + b * z < z := by linear_combination a * hxz + z * hab
    have key := hf hx hz hxy hyz
    field_simp [sub_pos.2 hxy, sub_pos.2 hyz] at key
    apply le_of_mul_le_mul_left ?_ (sub_pos.2 hxz)
    linear_combination key + (-f x * z + x * f z) * hab

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