slope_lt_rightDeriv — Mathlib

English

If f is strictly concave on S and x<y are in S, with f differentiable within at (Ioi x) at y, then the slope between x and y is strictly less than the right-derivative at y.

Русский

Если f строго вогнута на S и x<y в S, а производная f внутри Ioi x в точке y имеет значение f', то наклон секущей через x и y меньше правой производной в y.

LaTeX

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

Lean4

theorem slope_lt_rightDeriv (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hfd : DifferentiableWithinAt ℝ f (Ioi x) x) : slope f x y < derivWithin f (Ioi x) x :=
  hfc.slope_lt_of_hasDerivWithinAt_Ioi hx hy hxy hfd.hasDerivWithinAt

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