English
If f has a local maximum on s at a and y lies in pos tangent cone, then the derivative restricted to s at a in direction y is nonpositive.
Русский
Если у f локальный максимум на s в a и y лежит в pos tangent cone, то производная по f внутри s в направлении y не положительная.
LaTeX
$$$ HasFDerivWithinAt f f' s a \\land y \\in posTangentConeAt s a \\Rightarrow f'(y) \\le 0$$$
Lean4
/-- If `f` has a local max on `s` at `a` and `y` belongs to the positive tangent cone
of `s` at `a`, then `f' y ≤ 0`. -/
theorem fderivWithin_nonpos (h : IsLocalMaxOn f 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_nonpos hf.hasFDerivWithinAt hy
else by rw [fderivWithin_zero_of_not_differentiableWithinAt hf]; rfl
