lineDeriv_eq_zero — Mathlib

English

For an extr filter along a line, the line derivative is zero when the line tends to the limit along the filter.

Русский

Для фильтра экстремума вдоль линии производная вдоль этой линии обнуляется, когда прямая стремится к пределу по этому фильтру.

LaTeX

$$$\text{IsExtrFilter}(f,l,a) \land \text{Tendsto}(\lambda t. a + t\,b)(\mathcal{N}0)\ l \Rightarrow \text{lineDeriv}(f,a,b)=0$$$

Lean4

theorem lineDeriv_eq_zero {l : Filter E} (h : IsExtrFilter f l a) (h' : Tendsto (fun t : ℝ ↦ a + t • b) (𝓝 0) l) :
    lineDeriv ℝ f a b = 0 := by
  classical
    exact
    if hd : LineDifferentiableAt ℝ f a b then h.hasLineDerivAt_eq_zero hd.hasLineDerivAt h'
    else lineDeriv_zero_of_not_lineDifferentiableAt hd

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