isMinOn_of_rightDeriv_eq_zero — Mathlib

English

If convex on S and interior x with derivWithin f (Ioi x) x = 0, then x is a minimum on S.

Русский

Если f выпукла на S и interior x с derivWithin f(Ioi x) x = 0, то x — минимум на S.

LaTeX

$$$$ \ derivWithin f(Ioi x) x = 0 \Rightarrow IsMinOn\ f\ S\ x $$$$

Lean4

theorem isMinOn_of_rightDeriv_eq_zero (hf : ConvexOn ℝ S f) (hx : x ∈ interior S)
    (hf_rd : derivWithin f (Ioi x) x = 0) : IsMinOn f S x :=
  by
  refine hf.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg hx ?_ hf_rd.symm.le
  exact (hf.leftDeriv_le_rightDeriv_of_mem_interior hx).trans_eq hf_rd

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