deriv_lt_slope — Mathlib

English

If f is StrictConcaveOn on S, hx, hy ∈ S with x<y, and f is differentiable at y, then deriv f y < slope f x y.

Русский

Если fStrictConcaveOn на S, x,y ∈ S с x<y, и f дифференцируема в y, тогда deriv f y < slope f x y.

LaTeX

$$$\text{StrictConcaveOn}(\mathbb{R}, S, f)\land hx\in S\land hy\in S\land x

Lean4

theorem deriv_lt_slope (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hfd : DifferentiableAt ℝ f y) : deriv f y < slope f x y :=
  hfc.lt_slope_of_hasDerivAt hx hy hxy hfd.hasDerivAt

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