fderivWithin_eq_zero — Mathlib

English

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

Русский

Если локальный минимум существует, и y, -y лежат в pos tangent cone, то fderivWithin = 0.

LaTeX

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

Lean4

/-- If `f` has a local min on `s` at `a` and both `y` and `-y` belong to the positive tangent cone
of `s` at `a`, then `f' y = 0`. -/
theorem fderivWithin_eq_zero (h : IsLocalMinOn f s a) (hy : y ∈ posTangentConeAt s a)
    (hy' : -y ∈ posTangentConeAt s a) : (fderivWithin ℝ f s a : E → ℝ) y = 0 := by
  classical
    exact
    if hf : DifferentiableWithinAt ℝ f s a then h.hasFDerivWithinAt_eq_zero hf.hasFDerivWithinAt hy hy'
    else by rw [fderivWithin_zero_of_not_differentiableWithinAt hf]; rfl

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