English
If f is differentiable at x in the usual sense, then the line derivative equals the evaluation of the derivative at v.
Русский
Если f дифференцируема в обычном смысле в точке x, то линейная производная вдоль направления v равна применению производной к v.
LaTeX
$$$\text{DifferentiableAt}_{\mathbb{k}}(f,x) \Rightarrow \mathrm{lineDeriv}_{\mathbb{k}}(f,x,v) = fderiv_{\mathbb{k}}(f,x)(v)$$$
Lean4
theorem hasLineDerivWithinAt (hf : HasFDerivWithinAt f L s x) (v : E) : HasLineDerivWithinAt 𝕜 f (L v) s x v :=
by
let F := fun (t : 𝕜) ↦ x + t • v
rw [show x = F (0 : 𝕜) by simp [F]] at hf
have A : HasDerivWithinAt F (0 + (1 : 𝕜) • v) (F ⁻¹' s) 0 :=
((hasDerivAt_const (0 : 𝕜) x).add ((hasDerivAt_id' (0 : 𝕜)).smul_const v)).hasDerivWithinAt
simp only [one_smul, zero_add] at A
exact hf.comp_hasDerivWithinAt (x := (0 : 𝕜)) A (mapsTo_preimage F s)
