lt_slope_of_hasDerivWithinAt_Ioi — Mathlib

English

Let S be a subset of the real line and f : R → R be strictly convex on S. If x, y ∈ S with x < y and f has a right-hand derivative at x (i.e., the right derivative exists and equals f'), then the slope of the secant line joining (x, f(x)) and (y, f(y)) is strictly larger than f'.

Русский

Пусть S ⊆ R и f : R → R является строго выпуклой на S. Пусть x, y ∈ S и x < y, и если в точке x существует правая производная f′, то эта правая производная строго меньше наклона секантной прямой между точками (x, f(x)) и (y, f(y)).

LaTeX

$$$\text{If } S \subseteq \mathbb{R},\; f: \mathbb{R} \to \mathbb{R} \text{ is strictly convex on } S,\; x,y \in S,\; x

Lean4

/-- If `f : ℝ → ℝ` is strictly convex on `S` and right-differentiable at `x ∈ S`, then the slope of
any secant line with left endpoint at `x` is strictly greater than the right derivative of `f` at
`x`. -/
theorem lt_slope_of_hasDerivWithinAt_Ioi (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hf' : HasDerivWithinAt f f' (Ioi x) x) : f' < slope f x y :=
  by
  obtain ⟨u, hxu, huy⟩ := exists_between hxy
  have hu : u ∈ S := hfc.1.ordConnected.out hx hy ⟨hxu.le, huy.le⟩
  have := hfc.secant_strict_mono hx hu hy hxu.ne' hxy.ne' huy
  simp only [← slope_def_field] at this
  exact (hfc.convexOn.le_slope_of_hasDerivWithinAt_Ioi hx hu hxu hf').trans_lt this

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