slope_lt_of_hasDerivWithinAt_Iio — Mathlib

English

If f is strictly convex on S and differentiable from the left at y ∈ S, then the slope from x to y (x<y) is strictly less than the left derivative of f at y.

Русский

Если f строго выпукла на S и дифференцируема слева в y ∈ S, то наклон секанта между x и y меньше левой производной в y, при x<y.

LaTeX

$$$\text{If } x

Lean4

/-- If `f : ℝ → ℝ` is strictly convex on `S` and differentiable at `y ∈ S`, then the slope of any
secant line with right endpoint at `y` is strictly less than the left derivative at `y`. -/
theorem slope_lt_of_hasDerivWithinAt_Iio (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hf' : HasDerivWithinAt f f' (Iio y) y) : slope f x y < f' :=
  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 hy hx hu hxy.ne huy.ne hxu
  simp_rw [← slope_def_field, slope_comm _ y] at this
  exact this.trans_le <| hfc.convexOn.slope_le_of_hasDerivWithinAt_Iio hu hy huy hf'

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