strictConvexOn_iff_slope_strict_mono_adjacent

English

If the slope inequalities hold for all x<y<z with x,z in s for a strictly convex f, then the secant slopes are strictly increasing with the right endpoint: (f(y)-f(x))/(y-x) < (f(z)-f(y))/(z-y).

Русский

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

LaTeX

$$$\text{StrictConvexOn } 𝕜\ s\ f \Rightarrow \forall x,y,z:\ x∈s, z∈s, x

Lean4

/-- A function `f : 𝕜 → 𝕜` is strictly convex iff 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]`. -/
theorem strictConvexOn_iff_slope_strict_mono_adjacent :
    StrictConvexOn 𝕜 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_strict_mono_adjacent⟩, fun h =>
    strictConvexOn_of_slope_strict_mono_adjacent h.1 (@fun _ _ _ hx hy => h.2 hx hy)⟩

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