From 72ce984d032282c736175e1e38398d9508478993 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 23 Apr 2024 21:20:50 +0200
Subject: [PATCH] Update test.lean

---
 nevanlinna/test.lean | 29 ++++++++++++++++++++++++++---
 1 file changed, 26 insertions(+), 3 deletions(-)

diff --git a/nevanlinna/test.lean b/nevanlinna/test.lean
index 0cd2534..1bf0961 100644
--- a/nevanlinna/test.lean
+++ b/nevanlinna/test.lean
@@ -46,10 +46,33 @@ theorem SimpleCauchyFormula :
 theorem JensenFormula₂ :
   ∀
   {R : ℝ} -- Radius of the ball
-  {w : ℂ} -- Point in the interior of the ball
   {f : ℂ → ℂ}, -- Holomorphic function
   Differentiable ℂ f
-  → ∀ z ∈ Metric.ball 0 R, f z ≠ 0
-  → (∮ (z : ℂ) in C(0, R), Complex.log ‖f z‖ ) = 2 * π * R * log ‖f 0‖ := by
+  → (∀ z ∈ Metric.ball 0 R, f z ≠ 0)
+  → (∫ (θ : ℝ) in Set.Icc 0 (2 * π), Complex.log ‖f (circleMap 0 R θ)‖ ) = 2 * π * log ‖f 0‖ := by
+
+  intro r f fHyp₁ fHyp₂
+
+  have : (fun θ ↦ Complex.log ↑‖f (circleMap 0 r θ)‖) = (fun θ ↦ ((deriv (circleMap 0 r) θ)) • ((deriv (circleMap 0 r) θ)⁻¹ • Complex.log ↑‖f (circleMap 0 r θ)‖)) := by
+    funext θ
+    rw [← smul_assoc]
+
+    rw [smul_eq_mul, smul_eq_mul]
+    rw [mul_inv_cancel, one_mul]
+
+    simp
+
+    sorry
+
+  rw [this]
+
+  simp
+
+  let XX := circleIntegral_def_Icc (fun z ↦ -(Complex.I * z⁻¹ * (Complex.log ↑‖f z‖))) 0 r
+  simp at XX
+
+  rw [← XX]
+
+
 
   sorry