Partial derivatives commute

theorem fderiv_fderiv_comm {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E × F → G} {z : E × F} {dx : E} {dy : F} (sf : ContDiff ℝ 2 f) : (fderiv ℝ (fun (x : E) => (fderiv ℝ (fun (y : F) => f (x, y)) z.2) dy) z.1) dx = (fderiv ℝ (fun (y : F) => (fderiv ℝ (fun (x : E) => f (x, y)) z.1) dx) z.2) dy

theorem deriv_deriv_comm {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ × ℝ → E} {z : ℝ × ℝ} (sf : ContDiff ℝ 2 f) : deriv (fun (x : ℝ) => deriv (fun (y : ℝ) => f (x, y)) z.2) z.1 = deriv (fun (y : ℝ) => deriv (fun (x : ℝ) => f (x, y)) z.1) z.2

theorem ContDiff.iteratedDeriv_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {m : WithTop ℕ∞} {n : ℕ∞} {i : ℕ} (hf : ContDiff 𝕜 (↑n) f) (hmn : m + ↑i ≤ ↑n) : ContDiff 𝕜 m (_root_.iteratedDeriv i f)

theorem ContDiff.deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → 𝕜 → F} {g : E → 𝕜} {m : WithTop ℕ∞} (fc : ContDiff 𝕜 ⊤ (Function.uncurry f)) (gc : ContDiff 𝕜 ⊤ g) : ContDiff 𝕜 m fun (z : E) => _root_.deriv (fun (y : 𝕜) => f z y) (g z)

theorem ContDiff.iteratedDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → 𝕜 → F} {g : E → 𝕜} {m : WithTop ℕ∞} {n : ℕ} (fc : ContDiff 𝕜 ⊤ (Function.uncurry f)) (gc : ContDiff 𝕜 ⊤ g) : ContDiff 𝕜 m fun (z : E) => _root_.iteratedDeriv n (fun (y : 𝕜) => f z y) (g z)

theorem deriv_iteratedDeriv_comm {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ × ℝ → E} {z : ℝ × ℝ} (fc : ContDiff ℝ ⊤ f) (n : ℕ) : deriv (fun (x : ℝ) => iteratedDeriv n (fun (y : ℝ) => f (x, y)) z.2) z.1 = iteratedDeriv n (fun (y : ℝ) => deriv (fun (x : ℝ) => f (x, y)) z.1) z.2