Working…

nevanlinna/test.lean

@@ -84,13 +84,37 @@ theorem JensenFormula₂ :
     rw [this]
 
 
-  have : ∀ z : ℂ, Complex.log (Complex.abs z) = 1/2 * Complex.log z + 1/2 * Complex.log (conj z) := by
+  have : ∀ z : ℂ, 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]
+    by_cases argHyp : Complex.arg z = π 
+    
+    · rw [Complex.log, argHyp, Complex.log]
+      let ZZ := Complex.arg_conj z
+      rw [argHyp] at ZZ
+      
+      simp at ZZ
+
+      have : conj z = z := by
+        apply?
+        sorry
+
+    let ZZ := Complex.log_conj z
+
+    nth_rewrite 1 [Complex.log]
+    
+    simp
+
+    let φ := Complex.arg z
+    let r := Complex.abs z
+    have : z = r * Complex.exp (φ * Complex.I) := by
+      exact (Complex.abs_mul_exp_arg_mul_I z).symm
+
+    have : Complex.log z = Complex.log r + r*Complex.I := by
+      apply?
+      sorry
+    simp at XX
+
 
     sorry