Interchanging higher derivatives and pullbacks

For a C^(n+1) function, differentiating a fixed n-th directional derivative and performing those derivatives on its Fréchet derivative give the same linear map. Over real Hilbert spaces this also identifies the corresponding adjoint maps, which is the calculus step needed when training on derivatives. The results do not assume tensor shapes or a graph.

theorem Proofs.Autograd.iteratedFDeriv_fderiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : E → F} (hf : ContDiff 𝕜 (↑n + 1) f) (x v : E) (directions : Fin n → E) : (iteratedFDeriv 𝕜 n (fun (y : E) => (fderiv 𝕜 f y) v) x) directions = (fderiv 𝕜 (fun (y : E) => (iteratedFDeriv 𝕜 n f y) directions) x) v

A fixed directional derivative commutes with n further derivatives of a C^(n+1) map. The directions can repeat. The induction uses symmetry of the second derivative, so no analyticity assumption or permutation of a formal power series is needed.

theorem Proofs.Autograd.iteratedFDeriv_fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : E → F} (hf : ContDiff 𝕜 (↑n + 1) f) (x : E) (directions : Fin n → E) : (iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) directions = fderiv 𝕜 (fun (y : E) => (iteratedFDeriv 𝕜 n f y) directions) x

Taking the Fréchet derivative commutes with a fixed tuple of higher derivative directions.

theorem Proofs.Autograd.iteratedFDeriv_adjoint_fderiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [InnerProductSpace ℝ F] [CompleteSpace E] [CompleteSpace F] {n : ℕ} {f : E → F} (hf : ContDiff ℝ (↑n + 1) f) (x : E) (directions : Fin n → E) (seed : F) : (iteratedFDeriv ℝ n (fun (y : E) => (ContinuousLinearMap.adjoint (fderiv ℝ f y)) seed) x) directions = (ContinuousLinearMap.adjoint (fderiv ℝ (fun (y : E) => (iteratedFDeriv ℝ n f y) directions) x)) seed

Higher derivatives of a real pullback equal the pullback of the higher derivative. The cotangent and direction tuple are held constant; allowing them to vary would add terms.