Analyticity of iterated vertical slice derivatives

Mathlib proves that the n-fold iterate deriv^[n] f of an analytic function f : 𝕜 → F into a complete normed space is analytic (AnalyticAt.iterated_deriv). This file proves the parametric two-variable version for iteratedDeriv: if f : E × 𝕜 → F is jointly analytic at p, then (q : E × 𝕜) ↦ iteratedDeriv n (fun y ↦ f (q.1, y)) q.2 is jointly analytic at p (AnalyticAt.iteratedDeriv_snd), and in particular the vertical Taylor coefficient x ↦ iteratedDeriv n (fun y ↦ f (x, y)) p.2 is analytic at p.1 (AnalyticAt.curry_left_iteratedDeriv_snd).

theorem AnalyticAt.iteratedDeriv_snd {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E × 𝕜 → F} {p : E × 𝕜} (hf : AnalyticAt 𝕜 f p) (n : ℕ) : AnalyticAt 𝕜 (fun (q : E × 𝕜) => iteratedDeriv n (fun (y : 𝕜) => f (q.1, y)) q.2) p

If f : E × 𝕜 → F is jointly analytic at p and F is complete, then the n-th iterated derivative in the second variable (q : E × 𝕜) ↦ iteratedDeriv n (fun y ↦ f (q.1, y)) q.2 is jointly analytic at p.

theorem AnalyticAt.curry_left_iteratedDeriv_snd {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E × 𝕜 → F} {p : E × 𝕜} (hf : AnalyticAt 𝕜 f p) (n : ℕ) : AnalyticAt 𝕜 (fun (x : E) => iteratedDeriv n (fun (y : 𝕜) => f (x, y)) p.2) p.1

If f : E × 𝕜 → F is jointly analytic at p and F is complete, then x ↦ iteratedDeriv n (fun y ↦ f (x, y)) p.2 is analytic at p.1.