From a34699ddbc3b1b7faae96cae22c2b4800b46ccfc Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 5 Jun 2024 10:19:09 +0200
Subject: [PATCH] Create holomorphic.lean

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

diff --git a/Nevanlinna/holomorphic.lean b/Nevanlinna/holomorphic.lean
new file mode 100644
index 0000000..3f0330d
--- /dev/null
+++ b/Nevanlinna/holomorphic.lean
@@ -0,0 +1,63 @@
+import Mathlib.Analysis.Complex.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Defs
+import Nevanlinna.partialDeriv
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
+
+
+def HolomorphicAt (f : E → F) (x : E) : Prop :=
+  ∃ s ∈ nhds x, ∀ z ∈ s, DifferentiableAt ℂ f z
+
+
+theorem HolomorphicAt_iff
+  {f : E → F}
+  {x : E} :
+  HolomorphicAt f x ↔ ∃ s : Set E, IsOpen s ∧ x ∈ s ∧ (∀ z ∈ s, DifferentiableAt ℂ f z) := by
+  constructor
+  · intro hf
+    obtain ⟨t, h₁t, h₂t⟩ := hf
+    obtain ⟨s, h₁s, h₂s, h₃s⟩ := mem_nhds_iff.1 h₁t
+    use s
+    constructor
+    · assumption
+    · constructor
+      · assumption
+      · intro z hz
+        exact h₂t z (h₁s hz)
+  · intro hyp
+    obtain ⟨s, h₁s, h₂s, hf⟩ := hyp
+    use s
+    constructor
+    · apply (IsOpen.mem_nhds_iff h₁s).2 h₂s
+    · assumption
+
+
+theorem CauchyRiemann₅
+  {f : ℂ → F}
+  {z : ℂ} :
+  (DifferentiableAt ℂ f z) → partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by
+  intro h
+  unfold partialDeriv
+
+  conv =>
+    left
+    rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
+    simp
+    rw [← mul_one Complex.I]
+    rw [← smul_eq_mul]
+    rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f z) Complex.I 1]
+  conv =>
+    right
+    right
+    rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
+
+
+theorem CauchyRiemann₆
+  {f : ℂ → ℂ}
+  {z : ℂ} :
+  (HolomorphicAt f z) → partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by
+
+
+
+  sorry