English
Line differentiability along a direction v at a point x means the map t ↦ f(x + t v) is differentiable at t = 0; i.e., the line derivative exists in direction v at x.
Русский
Линейная производная по направлению v существует, если карта t ↦ f(x + t v) дифференцируема в t = 0; то есть существует линейное отображение производной вдоль направления.
LaTeX
$$$$\text{LineDifferentiableAt } f x v := \text{DifferentiableAt } 𝕜 (t \mapsto f(x + t v)) (0).$$$$
Lean4
/-- `f` has the derivative `f'` at the point `x` along the direction `v`.
That is, `f (x + t v) = f x + t • f' + o (t)` when `t` tends to `0`.
Note that this definition is less well behaved than the total Fréchet derivative, which
should generally be favored over this one. -/
def HasLineDerivAt (f : E → F) (f' : F) (x : E) (v : E) :=
HasDerivAt (fun t ↦ f (x + t • v)) f' (0 : 𝕜)
