isMinOn_of_leftDeriv_eq_zero — Mathlib

English

If convexOn and interior x with left-derivative equal to 0, then x minimizes f on S.

Русский

Если f выпукла на S, x ∈ interior S и левая производная равна нулю, то x — минимум на S.

LaTeX

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

Lean4

theorem isMinOn_of_leftDeriv_eq_zero (hf : ConvexOn ℝ S f) (hx : x ∈ interior S) (hf_ld : derivWithin f (Iio x) x = 0) :
    IsMinOn f S x := by
  refine hf.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg hx hf_ld.le ?_
  exact hf_ld.symm.le.trans (hf.leftDeriv_le_rightDeriv_of_mem_interior hx)

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