Directional derivatives

For a function f : 𝕜 → F of one variable, the directional derivative in the direction 1 is the ordinary derivative. This identifies the weak directional derivatives of TauCeti.HasWeakLineDerivOn on the real line with one-variable derivatives.

Outside the topological support of a function, its directional derivatives vanish. This is the directional counterpart of Mathlib's fderiv_of_notMem_tsupport. Both results require no differentiability hypothesis, which matters for Lipschitz functions.

The average y ↦ ∫₀¹ g (y - t h) dt of translates of a continuous real function g has directional derivative g y - g (y - h) in the direction h, by the fundamental theorem of calculus.

@[simp]

theorem TauCeti.lineDeriv_one {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} : lineDeriv 𝕜 f x 1 = deriv f x

The directional derivative of a function of one variable in the direction 1 is its derivative. No differentiability hypothesis is needed.

@[simp]

theorem TauCeti.lineDeriv_of_notMem_tsupport {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → F} {x : E} (h : x ∉ tsupport f) (v : E) : lineDeriv 𝕜 f x v = 0

Outside the topological support of f, every directional derivative of f vanishes. No differentiability hypothesis is needed.

theorem Continuous.hasLineDerivAt_intervalIntegral_comp_sub {E : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] {h : E} {g : E → G} (hg : Continuous g) (y : E) : HasLineDerivAt ℝ (fun (y : E) => ∫ (t : ℝ) in 0..1, g (y - t • h)) (g y - g (y - h)) y h

The function y ↦ ∫₀¹ g (y - t h) dt of a continuous g has directional derivative g y - g (y - h) in the direction h.