Update test.lean

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 ∈ Metric.ball 0 R, f z ≠ 0)
-  → (∮ (z : ℂ) in C(0, R), Complex.log ‖f z‖ ) = 2 * π * R * log ‖f 0‖ := by
+  → (∫ (θ : ℝ) 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