hasLineDerivAt_iff_isLittleO_nhds_zero

English

The line derivative exists with slope f′ if and only if the increment f(x+t v) − f(x) − t f′ tends to zero faster than t as t → 0; i.e., the little-o condition holds.

Русский

Линейная производная существует с наклоном f′ тогда, когда при стремлении t к 0 разность f(x+t v) − f(x) − t f′ становится большей скоростью, чем t (малая-o скорость).

LaTeX

$$$ HasLineDerivAt 𝕜 f f' x v \\iff (f(x + t v) - f(x) - t f') =o[𝓝 0] t $$$

Lean4

theorem hasLineDerivAt_iff_isLittleO_nhds_zero :
    HasLineDerivAt 𝕜 f f' x v ↔ (fun t : 𝕜 => f (x + t • v) - f x - t • f') =o[𝓝 0] fun t => t := by
  simp only [HasLineDerivAt, hasDerivAt_iff_isLittleO_nhds_zero, zero_add, zero_smul, add_zero]

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