English
If HasLineDerivAt holds, then the line derivative equals the value of the derivative along v at x; i.e., the line derivative is unique when it exists.
Русский
Если существует линейная производная по направлению, то она равна значению производной вдоль направления; производная по линии уникальна при существовании.
LaTeX
$$$$\text{HasLineDerivAt } 𝕜 f f' x v \Rightarrow \text{lineDeriv } 𝕜 f x v = f'.$$$$
Lean4
/-- Line derivative of `f` at the point `x` in the direction `v` within the set `s`, if it exists.
Zero otherwise.
If the line derivative exists (i.e., `∃ f', HasLineDerivWithinAt 𝕜 f f' s x v`), then
`f (x + t v) = f x + t lineDerivWithin 𝕜 f s x v + o (t)` when `t` tends to `0` and `x + t v ∈ s`.
-/
def lineDerivWithin (f : E → F) (s : Set E) (x : E) (v : E) : F :=
derivWithin (fun t ↦ f (x + t • v)) ((fun t ↦ x + t • v) ⁻¹' s) (0 : 𝕜)
