From e37ef6da161cb09d828ddc512ba40ecb0c6dba49 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 23 Apr 2024 10:03:36 +0200
Subject: [PATCH] Messing around

---
 nevanlinna/test.lean | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

diff --git a/nevanlinna/test.lean b/nevanlinna/test.lean
index 0849845..f92eb4f 100644
--- a/nevanlinna/test.lean
+++ b/nevanlinna/test.lean
@@ -1,3 +1,17 @@
-import Mathlib.Topology.Basic
+import Mathlib.Analysis.Complex.CauchyIntegral
 
-#check TopologicalSpace
+#check DiffContOnCl.circleIntegral_sub_inv_smul
+
+
+theorem CauchyIntegralFormula :
+  ∀
+  {R : ℝ} -- Radius of the ball
+  {w : ℂ} -- Point in the interior of the ball
+  {f : ℂ → ℂ}, -- Holomorphic function
+  DiffContOnCl ℂ f (Metric.ball 0 R)
+  → w ∈ Metric.ball 0 R
+  → (∮ (z : ℂ) in C(0, R), (z - w)⁻¹ • f z) = (2 * Real.pi * Complex.I) • f w := by
+
+  exact DiffContOnCl.circleIntegral_sub_inv_smul
+
+#check CauchyIntegralFormula