leftDeriv_eq_sSup_slope_of_mem_interior

English

If f is convex on S and x ∈ interior S, then the left derivative at x equals the supremum of the slopes from x to points to the left within S.

Русский

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

LaTeX

$$$$ \ derivWithin\ f\ (Iio\ x)\ x = \ sSup\ (\ image\ (slope\ f\ x)\ (\{y \mid y \in S \land y < x\})) $$$$

Lean4

theorem leftDeriv_eq_sSup_slope_of_mem_interior (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
    derivWithin f (Iio x) x = sSup (slope f x '' {y | y ∈ S ∧ y < x}) :=
  (hfc.hasDerivWithinAt_sSup_slope_of_mem_interior hxs).derivWithin (uniqueDiffWithinAt_Iio x)

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