English
Let E be a real normed vector space and f: E → ℝ. If a ∈ E is a local maximum of f, then the Fréchet derivative of f at a vanishes; in particular, if f is differentiable at a, then the derivative at a is zero.
Русский
Пусть E – реаловое нормированное векторное пространство, f: E → ℝ. Если a ∈ E является локальным максимумом функции f, то производная Фреше в точке a равна нулю; если в точке a функция дифференцируема, то производная в a равна нулю.
LaTeX
$$$\mathrm{LocalMax}(f,a) \Rightarrow f'(a) = 0$$$
Lean4
/-- **Fermat's Theorem**: the derivative of a function at a local maximum equals zero. -/
theorem fderiv_eq_zero (h : IsLocalMax f a) : fderiv ℝ f a = 0 := by
classical
exact
if hf : DifferentiableAt ℝ f a then h.hasFDerivAt_eq_zero hf.hasFDerivAt else fderiv_zero_of_not_differentiableAt hf
