hasDerivWithinAt_leftDeriv_of_mem_interior

English

Let f be convex on a set S and let x lie in the interior of S. Then f has a left-hand derivative at x (computed along the interval (-∞, x)), i.e. the left derivative is described by derivWithin f (Iio x) x.

Русский

Пусть f выпукла на множестве S и x ∈ interior S. Тогда в точке x существует левый производной производной f (по интервалу (-∞, x)); левый производный задаётся как derivWithin f(Iio x) x.

LaTeX

$$$$ HasDerivWithinAt\ f\ (\derivWithin\ f\ (Iio\ x)\ x)\ (Iio\ x)\ x $$$$

Lean4

theorem hasDerivWithinAt_leftDeriv_of_mem_interior (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
    HasDerivWithinAt f (derivWithin f (Iio x) x) (Iio x) x :=
  (hfc.differentiableWithinAt_Iio_of_mem_interior hxs).hasDerivWithinAt

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