English
If f has a local maximum on s at a, and y lies in the positive tangent cone, then fderivWithin ℝ f s a evaluated at y is nonpositive.
Русский
Если f имеет локальный максимум на s в точке a, и y принадлежит положительному касательному конусу, тогда fderivWithin f по a в точке y не положительно.
LaTeX
$$$(fderivWithin\\;\\mathbb{R}\\; f\\; s\\; a)(y) \\le 0$$$
Lean4
/-- If `f` has a local max 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 `f' y ≤ 0`. -/
theorem hasFDerivWithinAt_nonpos (h : IsLocalMaxOn f s a) (hf : HasFDerivWithinAt f f' s a)
(hy : y ∈ posTangentConeAt s a) : f' y ≤ 0 :=
by
rcases hy with ⟨c, d, hd, hc, hcd⟩
have hc' : Tendsto (‖c ·‖) atTop atTop := tendsto_abs_atTop_atTop.comp hc
suffices ∀ᶠ n in atTop, c n • (f (a + d n) - f a) ≤ 0 from le_of_tendsto (hf.lim atTop hd hc' hcd) this
replace hd : Tendsto (fun n => a + d n) atTop (𝓝[s] (a + 0)) :=
tendsto_nhdsWithin_iff.2 ⟨tendsto_const_nhds.add (tangentConeAt.lim_zero _ hc' hcd), hd⟩
rw [add_zero] at hd
filter_upwards [hd.eventually h, hc.eventually_ge_atTop 0] with n hfn hcn
exact mul_nonpos_of_nonneg_of_nonpos hcn (sub_nonpos.2 hfn)
