From b03954eee98c3583c658120759ae882d9cbd4d5e Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 6 May 2024 15:33:00 +0200
Subject: [PATCH] Create comparingDerivatives.lean

---
 Nevanlinna/comparingDerivatives.lean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 Nevanlinna/comparingDerivatives.lean

diff --git a/Nevanlinna/comparingDerivatives.lean b/Nevanlinna/comparingDerivatives.lean
new file mode 100644
index 0000000..7e7de02
--- /dev/null
+++ b/Nevanlinna/comparingDerivatives.lean
@@ -0,0 +1,17 @@
+import Mathlib.Data.Fin.Tuple.Basic
+import Mathlib.Analysis.Complex.Basic
+import Mathlib.Analysis.Complex.TaylorSeries
+import Mathlib.Analysis.Calculus.LineDeriv.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Defs
+import Mathlib.Analysis.Calculus.FDeriv.Basic
+import Mathlib.Analysis.Calculus.FDeriv.Symmetric
+
+
+lemma l₁ (f : ℝ × ℝ → ℝ) (h : ContDiff ℝ 2 f) :
+  ∀ z a b : ℝ × ℝ, (fderiv ℝ (fun w => fderiv ℝ f w) z) a b = iteratedFDeriv ℝ 2 f z ![a, b] := by
+  sorry
+
+lemma l₂ (f : ℝ × ℝ → ℝ) (h : ContDiff ℝ 2 f) :
+  ∀ z a b : ℝ × ℝ, (fderiv ℝ (fun w => fderiv ℝ f w) z) a b = (fderiv ℝ (fun w ↦ (fderiv ℝ f w) a) z) b := by
+  sorry
+