Update test.lean

nevanlinna/test.lean

@@ -1,4 +1,8 @@
 import Mathlib.Analysis.Complex.CauchyIntegral
+--import Mathlib.Analysis.Complex.Module
+
+
+open ComplexConjugate
 
 #check DiffContOnCl.circleIntegral_sub_inv_smul
 
@@ -18,7 +22,7 @@ theorem CauchyIntegralFormula :
 #check CauchyIntegralFormula
 #check HasDerivAt.continuousAt
 #check Real.log
-#check Complex.log
+#check ComplexConjugate.conj
 #check Complex.exp
 
 theorem SimpleCauchyFormula :
@@ -49,29 +53,52 @@ theorem JensenFormula₂ :
   {f : ℂ → ℂ}, -- Holomorphic function
   Differentiable ℂ f
   → (∀ z ∈ Metric.ball 0 R, f z ≠ 0)
-  → (∫ (θ : ℝ) in Set.Icc 0 (2 * π), Complex.log ‖f (circleMap 0 R θ)‖ ) = 2 * π * log ‖f 0‖ := by
+  → (∫ (θ : ℝ) in Set.Icc 0 (2 * π), Complex.log ‖f (circleMap 0 R θ)‖ ) = 2 * π * Complex.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]
+  /- We treat the trivial case r = 0 separately. -/
+  by_cases rHyp : r = 0
+  rw [rHyp]
+  simp
+  left
+  unfold ENNReal.ofReal
+  simp
+  rw [max_eq_left (mul_nonneg zero_le_two pi_nonneg)]
+  simp
+  /- From hereon, we assume that r ≠ 0. -/
 
-    rw [smul_eq_mul, smul_eq_mul]
-    rw [mul_inv_cancel, one_mul]
+  /- Replace the integral over 0 … 2π by a circle integral -/
+  suffices (∮ (z : ℂ) in C(0, r), -(Complex.I * z⁻¹ * Complex.log ↑(Complex.abs (f z)))) = 2 * ↑π * Complex.log ↑‖f 0‖ from by
+    have : ∫ (θ : ℝ) in Set.Icc 0 (2 * π), Complex.log ↑‖f (circleMap 0 r θ)‖ = (∮ (z : ℂ) in C(0, r), -(Complex.I * z⁻¹ * Complex.log ↑(Complex.abs (f z)))) := by
+      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, smul_eq_mul, smul_eq_mul, mul_inv_cancel, one_mul]
+        simp
+        exact rHyp
+      rw [this]
+      simp
+      let tmp := circleIntegral_def_Icc (fun z ↦ -(Complex.I * z⁻¹ * (Complex.log ↑‖f z‖))) 0 r
+      simp at tmp
+      rw [← tmp]
+    rw [this]
 
-    simp
+
+  have : ∀ z : ℂ, Complex.log (Complex.abs z) = 1/2 * Complex.log z + 1/2 * Complex.log (conj z) := by
+    intro z
+    have : ∃ r φ : ℝ, z = r * Complex.exp (φ * Complex.I) := by
+      sorry
+
+    obtain ⟨r, φ, h⟩ := this
+    rw [h]
 
     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]
+
+