hasFDerivWithinAt_nonneg — Mathlib

English

If a function has a local minimum on s at a and y lies in pos tangent cone, then fderivWithin at a in direction y is zero.

Русский

Если f имеет локальный минимум на s в a и y лежит в pos tangent cone, то fderivWithin по a вдоль y равна нулю.

LaTeX

$$$ fderivWithin \\(\\mathbb{R}\\; f\\; s\\; a\\; y = 0$$$

Lean4

/-- If `f` has a local min on `s` at `a`, `f'` is the derivative of `f` at `a` within `s`, and
`y` belongs to the positive tangent cone of `s` at `a`, then `0 ≤ f' y`. -/
theorem hasFDerivWithinAt_nonneg (h : IsLocalMinOn f s a) (hf : HasFDerivWithinAt f f' s a)
    (hy : y ∈ posTangentConeAt s a) : 0 ≤ f' y := by simpa using h.neg.hasFDerivWithinAt_nonpos hf.neg hy

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