English
If a local maximum exists and both y and -y lie in the positive tangent cone, then the fderivWithin equals zero.
Русский
Если существует локальный максимум и y, -y принадлежат положительному касательному конусу, то fderivWithin равна нулю.
LaTeX
$$$ fderivWithin \\(\\mathbb{R}\\; f\\; s\\; a\\; y = 0$$$
Lean4
/-- If `f` has a local max 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 : IsLocalMaxOn 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
