strictConvexOn_of_slope_strict_mono_adjacent

English

If f is strictly convex on s, then for any x<y<z in s the slope on [x,y] is strictly less than the slope on [y,z].

Русский

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

LaTeX

$$$\text{StrictConvexOn } 𝕜\ s\ f \Rightarrow \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
strictly less than the slope of the secant line of `f` on `[y, z]`, then `f` is strictly convex. -/
theorem strictConvexOn_of_slope_strict_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)) :
    StrictConvexOn 𝕜 s f :=
  LinearOrder.strictConvexOn_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 lt_of_mul_lt_mul_left ?_ (sub_pos.2 hxz).le
    linear_combination key + (-f x * z + x * f z) * hab

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