Messing around

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