rightDeriv_eq_sInf_slope_of_mem_interior

English

If f is convex on S and x ∈ interior S, then the right derivative of f at x (derivWithin f (Ioi x) x) equals the infimum of the slopes of secants emanating to the right from x with endpoints in S.

Русский

Пусть f выпукла на S и x ∈ interior S. Тогда правая производная f в x равна подпределу склонов секантных прямых, исходящих из x влево вправо с точками y ∈ S, y > x.

LaTeX

$$$$ \ derivWithin\ f\ (Ioi\ x)\ x = \ sInf\ ( sInf\ (\text{image} (\ slope\ f\ x)\ (\{y \mid y \in S \land x < y\})) ) $$$$

Lean4

theorem rightDeriv_eq_sInf_slope_of_mem_interior (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
    derivWithin f (Ioi x) x = sInf (slope f x '' {y | y ∈ S ∧ x < y}) :=
  (hfc.hasDerivWithinAt_sInf_slope_of_mem_interior hxs).derivWithin (uniqueDiffWithinAt_Ioi x)

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