Update specialFunctions_Integral_log_sin.lean

Nevanlinna/specialFunctions_Integral_log_sin.lean

@@ -208,16 +208,17 @@ lemma intervalIntegrable_log_sin₂ : IntervalIntegrable (log ∘ sin) volume 0
   simp at this
   exact one_le_pi_div_two
 
-lemma intervalIntegrable_log_sin : IntervalIntegrable (log ∘ sin) volume 0 π := by
+theorem intervalIntegrable_log_sin : IntervalIntegrable (log ∘ sin) volume 0 π := by
   apply IntervalIntegrable.trans (b := π / 2)
   exact intervalIntegrable_log_sin₂
+  -- IntervalIntegrable (log ∘ sin) volume (π / 2) π
   let A := IntervalIntegrable.comp_sub_left intervalIntegrable_log_sin₂ π
   simp at A
   let B := IntervalIntegrable.symm A
   have : π - π / 2 = π / 2 := by linarith
   rwa [this] at B
 
-lemma intervalIntegrable_log_cos : IntervalIntegrable (log ∘ cos) volume 0 (π / 2) := by
+theorem intervalIntegrable_log_cos : IntervalIntegrable (log ∘ cos) volume 0 (π / 2) := by
   let A := IntervalIntegrable.comp_sub_left intervalIntegrable_log_sin₂ (π / 2)
   simp only [Function.comp_apply, sub_zero, sub_self] at A
   simp_rw [sin_pi_div_two_sub] at A
@@ -225,28 +226,70 @@ lemma 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}
+  {g : ℝ → E}
+  {a : ℝ}
+  {b : ℝ}
+  (h₀ : a < b)
+  (h₁ : Set.EqOn f g (Set.Ioo a b)) :
+  ∫ (x : ℝ) in a..b, f x = ∫ (x : ℝ) in a..b, g x := by
+
+  apply intervalIntegral.integral_congr_ae
+  rw [MeasureTheory.ae_iff]
+  apply nonpos_iff_eq_zero.1
+  push_neg
+  have : {x | x ∈ Ι a b ∧ f x ≠ g x} ⊆ {b} := by
+    intro x hx
+    have t₂ : x ∈ Ι a b \ Set.Ioo a b := by
+      constructor
+      · exact hx.1
+      · by_contra H
+        exact hx.2 (h₁ H)
+    rw [Set.uIoc_of_le (le_of_lt h₀)] at t₂
+    rw [Set.Ioc_diff_Ioo_same h₀] at t₂
+    assumption
+  calc volume {a_1 | a_1 ∈ Ι a b ∧ f a_1 ≠ g a_1}
+  _ ≤ volume {b} := volume.mono this
+  _ = 0 := volume_singleton
+
 
 lemma integral_log_sin : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) =  -log 2 * π/2 := by
 
-  have t₀ {x : ℝ} : sin (2 * x) = 2 * sin x * cos x := sin_two_mul x
+  have t₁ {x : ℝ} : x ∈ Set.Ioo 0 (π / 2) → log (sin (2 * x)) = log 2 + log (sin x) + log (cos x) := by
+    intro hx
+    simp at hx
 
-  have t₁ {x : ℝ} : log (sin (2 * x)) = log 2 + log (sin x) + log (cos x) := by
     rw [sin_two_mul x, log_mul, log_mul]
     exact Ne.symm (NeZero.ne' 2)
-    sorry
-    sorry
-    sorry
+    -- sin x ≠ 0
+    apply (fun a => Ne.symm (ne_of_lt a))
+    apply sin_pos_of_mem_Ioo
+    constructor
+    · exact hx.1
+    · linarith [pi_pos, hx.2]
+    -- 2 * sin x ≠ 0
+    simp
+    apply (fun a => Ne.symm (ne_of_lt a))
+    apply sin_pos_of_mem_Ioo
+    constructor
+    · exact hx.1
+    · linarith [pi_pos, hx.2]
+    -- cos x ≠ 0
+    apply (fun a => Ne.symm (ne_of_lt a))
+    apply cos_pos_of_mem_Ioo
+    constructor
+    · linarith [pi_pos, hx.1]
+    · exact hx.2
 
-  have t₂ {x : ℝ} : log (sin x) = log (sin (2 * x)) - log 2 - log (cos x) := by
-    rw [t₁]
+  have t₂ : Set.EqOn (fun y ↦ log (sin y)) (fun y ↦ log (sin (2 * y)) - log 2 - log (cos y)) (Set.Ioo 0 (π / 2)) := by
+    intro x hx
+    simp
+    rw [t₁ hx]
     ring
 
-  conv =>
-    left
-    arg 1
-    intro x
-    rw [t₂]
-
+  rw [intervalIntegral.integral_congr_volume _ t₂]
   rw [intervalIntegral.integral_sub, intervalIntegral.integral_sub]
   rw [intervalIntegral.integral_const]
   rw [intervalIntegral.integral_comp_mul_left (c := 2) (f := fun x ↦ log (sin x))]
@@ -255,24 +298,57 @@ lemma integral_log_sin : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) =  -log 2 *
   rw [this]
 
   have : ∫ (x : ℝ) in (0)..π, log (sin x) = 2 * ∫ (x : ℝ) in (0)..(π / 2), log (sin x) := by
-    sorry
+    rw [← intervalIntegral.integral_add_adjacent_intervals (a := 0) (b := π / 2) (c := π)]
+    conv =>
+      left
+      right
+      arg 1
+      intro x
+      rw [← sin_pi_sub]
+    rw [intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)) π]
+    have : π - π / 2 = π / 2 := by linarith
     rw [this]
+    simp
+    ring
+    -- IntervalIntegrable (fun x => log (sin x)) volume 0 (π / 2)
+    exact intervalIntegrable_log_sin₂
+    -- IntervalIntegrable (fun x => log (sin x)) volume (π / 2) π
+    apply intervalIntegrable_log_sin.mono_set
+    rw [Set.uIcc_of_le, Set.uIcc_of_le]
+    apply Set.Icc_subset_Icc_left
+    linarith [pi_pos]
+    linarith [pi_pos]
+    linarith [pi_pos]
+  rw [this]
+
   have : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) = ∫ (x : ℝ) in (0)..(π / 2), log (cos x) := by
-    sorry
+    conv =>
+      right
+      arg 1
+      intro x
+      rw [← sin_pi_div_two_sub]
+    rw [intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)) (π / 2)]
+    simp
   rw [← this]
   simp
   linarith
 
   exact Ne.symm (NeZero.ne' 2)
   -- IntervalIntegrable (fun x => log (sin (2 * x))) volume 0 (π / 2)
-  sorry
+  let A := intervalIntegrable_log_sin.comp_mul_left 2
+  simp at A
+  assumption
   -- IntervalIntegrable (fun x => log 2) volume 0 (π / 2)
   simp
   -- IntervalIntegrable (fun x => log (sin (2 * x)) - log 2) volume 0 (π / 2)
   apply IntervalIntegrable.sub
   -- -- IntervalIntegrable (fun x => log (sin (2 * x))) volume 0 (π / 2)
-  sorry
+  let A := intervalIntegrable_log_sin.comp_mul_left 2
+  simp at A
+  assumption
   -- -- IntervalIntegrable (fun x => log 2) volume 0 (π / 2)
   simp
   -- -- IntervalIntegrable (fun x => log (cos x)) volume 0 (π / 2)
   exact intervalIntegrable_log_cos
+  --
+  linarith [pi_pos]