Create holomorphic.lean

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