hasFDerivWithinAt_eq_zero — Mathlib

English

If a local minimum exists and y, -y lie in pos tangent cone, then the derivative equals zero.

Русский

Если существует локальный минимум и y, -y принадлежат pos tangent cone, то производная равна нулю.

LaTeX

$$$ y \\in posTangentConeAt s a \\land -y \\in posTangentConeAt s a \\Rightarrow f' y = 0$$$

Lean4

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

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