From 0cc0c815085d6e924966b80ca18e55934ce92cbe Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 13 Aug 2024 10:25:03 +0200
Subject: [PATCH] Update specialFunctions_Integrals.lean

---
 Nevanlinna/specialFunctions_Integrals.lean | 51 +++++++++++-----------
 1 file changed, 26 insertions(+), 25 deletions(-)

diff --git a/Nevanlinna/specialFunctions_Integrals.lean b/Nevanlinna/specialFunctions_Integrals.lean
index 0ceb7da..657d37a 100644
--- a/Nevanlinna/specialFunctions_Integrals.lean
+++ b/Nevanlinna/specialFunctions_Integrals.lean
@@ -66,9 +66,10 @@ theorem logInt
 lemma int₁ :
   ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - 1‖ = 0 := by
 
-
-
-  have {x : ℝ} : Complex.normSq (circleMap 0 1 x - 1) = 2 - 2 * cos x := by
+  have {x : ℝ} : log ‖circleMap 0 1 x - 1‖ = log (4 * sin (x / 2) ^ 2) / 2 := by
+    dsimp [Complex.abs]
+    rw [log_sqrt (Complex.normSq_nonneg (circleMap 0 1 x - 1))]
+    congr
     calc Complex.normSq (circleMap 0 1 x - 1)
     _ = (cos x - 1) * (cos x - 1) + sin x * sin x := by
       dsimp [circleMap]
@@ -79,35 +80,35 @@ lemma int₁ :
     _ = 2 - 2 * cos x := by
       rw [sin_sq_add_cos_sq]
       norm_num
-
-
-  have {x : ℝ} : 2 - 2 * cos x = 4 * sin (x / 2) ^ 2 := by
-    calc 2 - 2 * cos x
     _ = 2 - 2 * cos (2 * (x / 2)) := by
       rw [← mul_div_assoc]
       congr; norm_num
     _ = 4 - 4 * Real.cos (x / 2) ^ 2 := by
       rw [cos_two_mul]
-      norm_num
+      ring
     _ = 4 * sin (x / 2) ^ 2 := by
-      nth_rw 1 [← mul_one 4]
-      nth_rw 1 [← sin_sq_add_cos_sq (x / 2)]
-      rw [mul_add]
-      abel
-
-
-
-
-
-
-  dsimp [Complex.abs]
-  sorry
-
-
-
-
-    sorry
+      nth_rw 1 [← mul_one 4, ← sin_sq_add_cos_sq (x / 2)]
+      ring
+  simp_rw [this]
+  simp
 
+  have : ∫ (x : ℝ) in (0)..2 * π, log (4 * sin (x / 2) ^ 2) =  2 * ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) := by
+    have : 1 = 2 * (2 : ℝ)⁻¹ := by exact Eq.symm (mul_inv_cancel_of_invertible 2)
+    nth_rw 1 [← one_mul (∫ (x : ℝ) in (0)..2 * π, log (4 * sin (x / 2) ^ 2))]
+    rw [← mul_inv_cancel_of_invertible 2, mul_assoc]
+    let f := fun y ↦ log (4 * sin y ^ 2)
+    have {x : ℝ} : log (4 * sin (x / 2) ^ 2) = f (x / 2) := by simp
+    conv =>
+      left
+      right
+      right
+      arg 1
+      intro x
+      rw [this]
+    rw [intervalIntegral.inv_mul_integral_comp_div 2]
+    simp
+  rw [this]
+  simp