From 23dfdd3716bafcd093f3c473416dabdf0a9c6569 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 15 Aug 2024 12:10:18 +0200
Subject: [PATCH] =?UTF-8?q?working=E2=80=A6?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 ...pecialFunctions_CircleIntegral_affine.lean | 33 ++++++++++++++++++-
 .../specialFunctions_Integral_log_sin.lean    |  9 +++--
 2 files changed, 38 insertions(+), 4 deletions(-)

diff --git a/Nevanlinna/specialFunctions_CircleIntegral_affine.lean b/Nevanlinna/specialFunctions_CircleIntegral_affine.lean
index fae2a66..4c2d790 100644
--- a/Nevanlinna/specialFunctions_CircleIntegral_affine.lean
+++ b/Nevanlinna/specialFunctions_CircleIntegral_affine.lean
@@ -2,6 +2,7 @@ import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
 import Mathlib.MeasureTheory.Integral.CircleIntegral
 import Mathlib.MeasureTheory.Measure.Restrict
+import Nevanlinna.specialFunctions_Integral_log_sin
 
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
@@ -10,7 +11,37 @@ open Real Filter MeasureTheory intervalIntegral
 
 
 lemma int₁₁ : ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) = 0 := by
-  sorry
+
+  have t₁ {x : ℝ} : x ∈ Set.Ioo 0 π → log (4 * sin x ^ 2) = log 4 + 2 * log (sin x) := by
+    intro hx
+    rw [log_mul, log_pow]
+    rfl
+    exact Ne.symm (NeZero.ne' 4)
+    apply pow_ne_zero 2
+    apply (fun a => Ne.symm (ne_of_lt a))
+    exact sin_pos_of_mem_Ioo hx
+
+
+  have t₂ : Set.EqOn (fun y ↦ log (4 * sin y ^ 2)) (fun y ↦ log 4 + 2 * log (sin y)) (Set.Ioo 0 π) := by
+    intro x hx
+    simp
+    rw [t₁ hx]
+
+  rw [intervalIntegral.integral_congr_volume pi_pos t₂]
+  rw [intervalIntegral.integral_add]
+  rw [intervalIntegral.integral_const_mul]
+  simp
+  rw [integral_log_sin₂]
+  have : (4 : ℝ) = 2 * 2 := by norm_num
+  rw [this, log_mul]
+  ring
+  norm_num
+  norm_num
+  -- IntervalIntegrable (fun x => log 4) volume 0 π
+  simp
+  -- IntervalIntegrable (fun x => 2 * log (sin x)) volume 0 π
+  apply IntervalIntegrable.const_mul
+  exact intervalIntegrable_log_sin
 
 
 lemma int₁ :
diff --git a/Nevanlinna/specialFunctions_Integral_log_sin.lean b/Nevanlinna/specialFunctions_Integral_log_sin.lean
index 3153c09..23c2cec 100644
--- a/Nevanlinna/specialFunctions_Integral_log_sin.lean
+++ b/Nevanlinna/specialFunctions_Integral_log_sin.lean
@@ -1,7 +1,5 @@
 import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
-import Mathlib.MeasureTheory.Integral.CircleIntegral
-import Mathlib.MeasureTheory.Measure.Restrict
 
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
@@ -226,6 +224,7 @@ theorem intervalIntegrable_log_cos : IntervalIntegrable (log ∘ cos) volume 0 (
   apply IntervalIntegrable.symm
   rwa [← this]
 
+
 theorem intervalIntegral.integral_congr_volume
   {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E]
   {f : ℝ → E}
@@ -255,7 +254,7 @@ theorem intervalIntegral.integral_congr_volume
   _ = 0 := volume_singleton
 
 
-lemma integral_log_sin : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) =  -log 2 * π/2 := by
+lemma integral_log_sin₁ : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) =  -log 2 * π/2 := by
 
   have t₁ {x : ℝ} : x ∈ Set.Ioo 0 (π / 2) → log (sin (2 * x)) = log 2 + log (sin x) + log (cos x) := by
     intro hx
@@ -352,3 +351,7 @@ lemma integral_log_sin : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) =  -log 2 *
   exact intervalIntegrable_log_cos
   --
   linarith [pi_pos]
+
+
+lemma integral_log_sin₂ : ∫ (x : ℝ) in (0)..π, log (sin x) =  -log 2 * π := by
+  sorry