diff --git a/Nevanlinna/specialFunctions_CircleIntegral_affine.lean b/Nevanlinna/specialFunctions_CircleIntegral_affine.lean
index 891bdfc..fae2a66 100644
--- a/Nevanlinna/specialFunctions_CircleIntegral_affine.lean
+++ b/Nevanlinna/specialFunctions_CircleIntegral_affine.lean
@@ -8,275 +8,6 @@ open Real Filter MeasureTheory intervalIntegral
 
 
 
-lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log ((π / 2)⁻¹ * x)‖ := by
-
-  intro x hx
-  by_cases h'x : x = 0
-  · rw [h'x]; simp
-
-  -- Now handle the case where x ≠ 0
-  have l₀ : log ((π / 2)⁻¹ * x) ≤ 0 := by
-    apply log_nonpos
-    apply mul_nonneg
-    apply le_of_lt
-    apply inv_pos.2
-    apply div_pos
-    exact pi_pos
-    exact zero_lt_two
-    apply (Set.mem_Icc.1 hx).1
-    simp
-    apply mul_le_one
-    rw [div_le_one pi_pos]
-    exact two_le_pi
-    exact (Set.mem_Icc.1 hx).1
-    exact (Set.mem_Icc.1 hx).2
-
-  have l₁ : 0 ≤ sin x := by
-    apply sin_nonneg_of_nonneg_of_le_pi (Set.mem_Icc.1 hx).1
-    trans (1 : ℝ)
-    exact (Set.mem_Icc.1 hx).2
-    trans π / 2
-    exact one_le_pi_div_two
-    norm_num [pi_nonneg]
-  have l₂ : log (sin x) ≤ 0 := log_nonpos l₁ (sin_le_one x)
-
-  simp only [norm_eq_abs, Function.comp_apply]
-  rw [abs_eq_neg_self.2 l₀]
-  rw [abs_eq_neg_self.2 l₂]
-  simp only [neg_le_neg_iff, ge_iff_le]
-
-  have l₃ : x ∈ (Set.Ioi 0) := by
-    simp
-    exact lt_of_le_of_ne (Set.mem_Icc.1 hx).1 ( fun a => h'x (id (Eq.symm a)) )
-
-  have l₅ : 0 < (π / 2)⁻¹ * x := by
-    apply mul_pos
-    apply inv_pos.2
-    apply div_pos pi_pos zero_lt_two
-    exact l₃
-
-  have : ∀ x ∈ (Set.Icc 0 (π / 2)), (π / 2)⁻¹ * x ≤ sin x := by
-    intro x hx
-
-    have i₀ : 0 ∈ Set.Icc 0 π :=
-      Set.left_mem_Icc.mpr pi_nonneg
-    have i₁ : π / 2 ∈ Set.Icc 0 π :=
-      Set.mem_Icc.mpr ⟨div_nonneg pi_nonneg zero_le_two, half_le_self pi_nonneg⟩
-
-    have i₂ : 0 ≤ 1 - (π / 2)⁻¹ * x := by
-      rw [sub_nonneg]
-      calc (π / 2)⁻¹ * x
-      _ ≤ (π / 2)⁻¹ * (π / 2) := by
-        apply mul_le_mul_of_nonneg_left
-        exact (Set.mem_Icc.1 hx).2
-        apply inv_nonneg.mpr (div_nonneg pi_nonneg zero_le_two)
-      _ = 1 := by
-        apply inv_mul_cancel
-        apply div_ne_zero_iff.mpr
-        constructor
-        · exact pi_ne_zero
-        · exact Ne.symm (NeZero.ne' 2)
-
-    have i₃ : 0 ≤ (π / 2)⁻¹ * x := by
-      apply mul_nonneg
-      apply inv_nonneg.2
-      apply div_nonneg
-      exact pi_nonneg
-      exact zero_le_two
-      exact (Set.mem_Icc.1 hx).1
-
-    have i₄ : 1 - (π / 2)⁻¹ * x + (π / 2)⁻¹ * x = 1 := by ring
-
-    let B := strictConcaveOn_sin_Icc.concaveOn.2 i₀ i₁ i₂ i₃ i₄
-    simp [Real.sin_pi_div_two] at B
-    rw [(by ring_nf; rw [mul_inv_cancel pi_ne_zero, one_mul] : 2 / π * x * (π / 2) = x)] at B
-    simpa
-
-  apply log_le_log l₅
-  apply this
-  apply Set.mem_Icc.mpr
-  constructor
-  · exact le_of_lt l₃
-  · trans 1
-    exact (Set.mem_Icc.1 hx).2
-    exact one_le_pi_div_two
-
-
-lemma intervalIntegrable_log_sin₁ : IntervalIntegrable (log ∘ sin) volume 0 1 := by
-
-  have int_log : IntervalIntegrable (fun x ↦ ‖log x‖) volume 0 1 := by
-    apply IntervalIntegrable.norm
-    rw [← neg_neg log]
-    apply IntervalIntegrable.neg
-    apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))
-    · exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg
-    · intro x hx
-      norm_num at hx
-      convert ((hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x)).neg using 1
-      norm_num
-    · intro x hx
-      norm_num at hx
-      rw [Pi.neg_apply, Left.nonneg_neg_iff]
-      exact (log_nonpos_iff hx.left).mpr hx.right.le
-
-
-  have int_log : IntervalIntegrable (fun x ↦ ‖log ((π / 2)⁻¹ * x)‖) volume 0 1 := by
-
-    have A := IntervalIntegrable.comp_mul_right int_log (π / 2)⁻¹
-    simp only [norm_eq_abs] at A
-    conv =>
-      arg 1
-      intro x
-      rw [mul_comm]
-    simp only [norm_eq_abs]
-    apply IntervalIntegrable.mono A
-    simp
-    trans Set.Icc 0 (π / 2)
-    exact Set.Icc_subset_Icc (Preorder.le_refl 0) one_le_pi_div_two
-    exact Set.Icc_subset_uIcc
-    exact Preorder.le_refl volume
-
-  apply IntervalIntegrable.mono_fun' (g := fun x ↦ ‖log ((π / 2)⁻¹ * x)‖)
-  exact int_log
-
-  -- AEStronglyMeasurable (log ∘ sin) (volume.restrict (Ι 0 1))
-  apply ContinuousOn.aestronglyMeasurable
-  apply ContinuousOn.comp (t := Ι 0 1)
-  apply ContinuousOn.mono (s := {0}ᶜ)
-  exact continuousOn_log
-  intro x hx
-  by_contra contra
-  simp at contra
-  rw [contra, Set.left_mem_uIoc] at hx
-  linarith
-  exact continuousOn_sin
-
-  -- Set.MapsTo sin (Ι 0 1) (Ι 0 1)
-  rw [Set.uIoc_of_le (zero_le_one' ℝ)]
-  exact fun x hx ↦ ⟨sin_pos_of_pos_of_le_one hx.1 hx.2, sin_le_one x⟩
-
-  -- MeasurableSet (Ι 0 1)
-  exact measurableSet_uIoc
-
-  -- (fun x => ‖(log ∘ sin) x‖) ≤ᶠ[ae (volume.restrict (Ι 0 1))] ‖log‖
-  dsimp [EventuallyLE]
-  rw [MeasureTheory.ae_restrict_iff]
-  apply MeasureTheory.ae_of_all
-  intro x hx
-  have : x ∈ Set.Icc 0 1 := by
-    simp
-    simp at hx
-    constructor
-    · exact le_of_lt hx.1
-    · exact hx.2
-  let A := logsinBound x this
-  simp only [Function.comp_apply, norm_eq_abs] at A
-  exact A
-
-  apply measurableSet_le
-  apply Measurable.comp'
-  exact continuous_abs.measurable
-  exact Measurable.comp' measurable_log continuous_sin.measurable
-  -- Measurable fun a => |log ((π / 2)⁻¹ * a)|
-  apply Measurable.comp'
-  exact continuous_abs.measurable
-  apply Measurable.comp'
-  exact measurable_log
-  exact measurable_const_mul (π / 2)⁻¹
-
-lemma intervalIntegrable_log_sin₂ : IntervalIntegrable (log ∘ sin) volume 0 (π / 2) := by
-
-  apply IntervalIntegrable.trans (b := 1)
-  exact intervalIntegrable_log_sin₁
-
-  -- IntervalIntegrable (log ∘ sin) volume 1 (π / 2)
-  apply ContinuousOn.intervalIntegrable
-  apply ContinuousOn.comp continuousOn_log continuousOn_sin
-  intro x hx
-  rw [Set.uIcc_of_le, Set.mem_Icc] at hx
-  have : 0 < sin x := by
-    apply Real.sin_pos_of_pos_of_lt_pi
-    · calc 0
-      _ < 1 := Real.zero_lt_one
-      _ ≤ x := hx.1
-    · calc x
-      _ ≤ π / 2 := hx.2
-      _ < π := div_two_lt_of_pos pi_pos
-  by_contra h₁x
-  simp at h₁x
-  rw [h₁x] at this
-  simp at this
-  exact one_le_pi_div_two
-
-lemma intervalIntegrable_log_sin : IntervalIntegrable (log ∘ sin) volume 0 π := by
-  apply IntervalIntegrable.trans (b := π / 2)
-  exact intervalIntegrable_log_sin₂
-  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
-  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
-  have : (fun x => log (cos x)) = log ∘ cos := rfl
-  apply IntervalIntegrable.symm
-  rwa [← this]
-
-
-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 : ℝ} : 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
-
-  have t₂ {x : ℝ} : log (sin x) = log (sin (2 * x)) - log 2 - log (cos x) := by
-    rw [t₁]
-    ring
-
-  conv =>
-    left
-    arg 1
-    intro x
-    rw [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))]
-  simp
-  have : 2 * (π / 2) = π := by linarith
-  rw [this]
-
-  have : ∫ (x : ℝ) in (0)..π, log (sin x) = 2 * ∫ (x : ℝ) in (0)..(π / 2), log (sin x) := by
-    sorry
-  rw [this]
-  have : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) = ∫ (x : ℝ) in (0)..(π / 2), log (cos x) := by
-    sorry
-  rw [← this]
-  simp
-  linarith
-
-  exact Ne.symm (NeZero.ne' 2)
-  -- IntervalIntegrable (fun x => log (sin (2 * x))) volume 0 (π / 2)
-  sorry
-  -- 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
-  -- -- IntervalIntegrable (fun x => log 2) volume 0 (π / 2)
-  simp
-  -- -- IntervalIntegrable (fun x => log (cos x)) volume 0 (π / 2)
-  exact intervalIntegrable_log_cos
-
 
 lemma int₁₁ : ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) = 0 := by
   sorry
diff --git a/Nevanlinna/specialFunctions_Integral_log.lean b/Nevanlinna/specialFunctions_Integral_log.lean
index 92dcdc4..9b8eaae 100644
--- a/Nevanlinna/specialFunctions_Integral_log.lean
+++ b/Nevanlinna/specialFunctions_Integral_log.lean
@@ -9,224 +9,6 @@ open Real Filter MeasureTheory intervalIntegral
 -- The following theorem was suggested by Gareth Ma on Zulip
 
 
-lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log ((π / 2)⁻¹ * x)‖ := by
-
-  intro x hx
-  by_cases h'x : x = 0
-  · rw [h'x]; simp
-
-  -- Now handle the case where x ≠ 0
-  have l₀ : log ((π / 2)⁻¹ * x) ≤ 0 := by
-    apply log_nonpos
-    apply mul_nonneg
-    apply le_of_lt
-    apply inv_pos.2
-    apply div_pos
-    exact pi_pos
-    exact zero_lt_two
-    apply (Set.mem_Icc.1 hx).1
-    simp
-    apply mul_le_one
-    rw [div_le_one pi_pos]
-    exact two_le_pi
-    exact (Set.mem_Icc.1 hx).1
-    exact (Set.mem_Icc.1 hx).2
-
-  have l₁ : 0 ≤ sin x := by
-    apply sin_nonneg_of_nonneg_of_le_pi (Set.mem_Icc.1 hx).1
-    trans (1 : ℝ)
-    exact (Set.mem_Icc.1 hx).2
-    trans π / 2
-    exact one_le_pi_div_two
-    norm_num [pi_nonneg]
-  have l₂ : log (sin x) ≤ 0 := log_nonpos l₁ (sin_le_one x)
-
-  simp only [norm_eq_abs, Function.comp_apply]
-  rw [abs_eq_neg_self.2 l₀]
-  rw [abs_eq_neg_self.2 l₂]
-  simp only [neg_le_neg_iff, ge_iff_le]
-
-  have l₃ : x ∈ (Set.Ioi 0) := by
-    simp
-    exact lt_of_le_of_ne (Set.mem_Icc.1 hx).1 ( fun a => h'x (id (Eq.symm a)) )
-
-  have l₅ : 0 < (π / 2)⁻¹ * x := by
-    apply mul_pos
-    apply inv_pos.2
-    apply div_pos pi_pos zero_lt_two
-    exact l₃
-
-  have : ∀ x ∈ (Set.Icc 0 (π / 2)), (π / 2)⁻¹ * x ≤ sin x := by
-    intro x hx
-
-    have i₀ : 0 ∈ Set.Icc 0 π :=
-      Set.left_mem_Icc.mpr pi_nonneg
-    have i₁ : π / 2 ∈ Set.Icc 0 π :=
-      Set.mem_Icc.mpr ⟨div_nonneg pi_nonneg zero_le_two, half_le_self pi_nonneg⟩
-
-    have i₂ : 0 ≤ 1 - (π / 2)⁻¹ * x := by
-      rw [sub_nonneg]
-      calc (π / 2)⁻¹ * x
-      _ ≤ (π / 2)⁻¹ * (π / 2) := by
-        apply mul_le_mul_of_nonneg_left
-        exact (Set.mem_Icc.1 hx).2
-        apply inv_nonneg.mpr (div_nonneg pi_nonneg zero_le_two)
-      _ = 1 := by
-        apply inv_mul_cancel
-        apply div_ne_zero_iff.mpr
-        constructor
-        · exact pi_ne_zero
-        · exact Ne.symm (NeZero.ne' 2)
-
-    have i₃ : 0 ≤ (π / 2)⁻¹ * x := by
-      apply mul_nonneg
-      apply inv_nonneg.2
-      apply div_nonneg
-      exact pi_nonneg
-      exact zero_le_two
-      exact (Set.mem_Icc.1 hx).1
-
-    have i₄ : 1 - (π / 2)⁻¹ * x + (π / 2)⁻¹ * x = 1 := by ring
-
-    let B := strictConcaveOn_sin_Icc.concaveOn.2 i₀ i₁ i₂ i₃ i₄
-    simp [Real.sin_pi_div_two] at B
-    rw [(by ring_nf; rw [mul_inv_cancel pi_ne_zero, one_mul] : 2 / π * x * (π / 2) = x)] at B
-    simpa
-
-  apply log_le_log l₅
-  apply this
-  apply Set.mem_Icc.mpr
-  constructor
-  · exact le_of_lt l₃
-  · trans 1
-    exact (Set.mem_Icc.1 hx).2
-    exact one_le_pi_div_two
-
-
-lemma intervalIntegrable_log_sin₁ : IntervalIntegrable (log ∘ sin) volume 0 1 := by
-
-  have int_log : IntervalIntegrable (fun x ↦ ‖log x‖) volume 0 1 := by
-    apply IntervalIntegrable.norm
-    rw [← neg_neg log]
-    apply IntervalIntegrable.neg
-    apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))
-    · exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg
-    · intro x hx
-      norm_num at hx
-      convert ((hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x)).neg using 1
-      norm_num
-    · intro x hx
-      norm_num at hx
-      rw [Pi.neg_apply, Left.nonneg_neg_iff]
-      exact (log_nonpos_iff hx.left).mpr hx.right.le
-
-
-  have int_log : IntervalIntegrable (fun x ↦ ‖log ((π / 2)⁻¹ * x)‖) volume 0 1 := by
-
-    have A := IntervalIntegrable.comp_mul_right int_log (π / 2)⁻¹
-    simp only [norm_eq_abs] at A
-    conv =>
-      arg 1
-      intro x
-      rw [mul_comm]
-    simp only [norm_eq_abs]
-    apply IntervalIntegrable.mono A
-    simp
-    trans Set.Icc 0 (π / 2)
-    exact Set.Icc_subset_Icc (Preorder.le_refl 0) one_le_pi_div_two
-    exact Set.Icc_subset_uIcc
-    exact Preorder.le_refl volume
-
-  apply IntervalIntegrable.mono_fun' (g := fun x ↦ ‖log ((π / 2)⁻¹ * x)‖)
-  exact int_log
-
-  -- AEStronglyMeasurable (log ∘ sin) (volume.restrict (Ι 0 1))
-  apply ContinuousOn.aestronglyMeasurable
-  apply ContinuousOn.comp (t := Ι 0 1)
-  apply ContinuousOn.mono (s := {0}ᶜ)
-  exact continuousOn_log
-  intro x hx
-  by_contra contra
-  simp at contra
-  rw [contra, Set.left_mem_uIoc] at hx
-  linarith
-  exact continuousOn_sin
-
-  -- Set.MapsTo sin (Ι 0 1) (Ι 0 1)
-  rw [Set.uIoc_of_le (zero_le_one' ℝ)]
-  exact fun x hx ↦ ⟨sin_pos_of_pos_of_le_one hx.1 hx.2, sin_le_one x⟩
-
-  -- MeasurableSet (Ι 0 1)
-  exact measurableSet_uIoc
-
-  -- (fun x => ‖(log ∘ sin) x‖) ≤ᶠ[ae (volume.restrict (Ι 0 1))] ‖log‖
-  dsimp [EventuallyLE]
-  rw [MeasureTheory.ae_restrict_iff]
-  apply MeasureTheory.ae_of_all
-  intro x hx
-  have : x ∈ Set.Icc 0 1 := by
-    simp
-    simp at hx
-    constructor
-    · exact le_of_lt hx.1
-    · exact hx.2
-  let A := logsinBound x this
-  simp only [Function.comp_apply, norm_eq_abs] at A
-  exact A
-
-  apply measurableSet_le
-  apply Measurable.comp'
-  exact continuous_abs.measurable
-  exact Measurable.comp' measurable_log continuous_sin.measurable
-  -- Measurable fun a => |log ((π / 2)⁻¹ * a)|
-  apply Measurable.comp'
-  exact continuous_abs.measurable
-  apply Measurable.comp'
-  exact measurable_log
-  exact measurable_const_mul (π / 2)⁻¹
-
-lemma intervalIntegrable_log_sin₂ : IntervalIntegrable (log ∘ sin) volume 0 (π / 2) := by
-
-  apply IntervalIntegrable.trans (b := 1)
-  exact intervalIntegrable_log_sin₁
-
-  -- IntervalIntegrable (log ∘ sin) volume 1 (π / 2)
-  apply ContinuousOn.intervalIntegrable
-  apply ContinuousOn.comp continuousOn_log continuousOn_sin
-  intro x hx
-  rw [Set.uIcc_of_le, Set.mem_Icc] at hx
-  have : 0 < sin x := by
-    apply Real.sin_pos_of_pos_of_lt_pi
-    · calc 0
-      _ < 1 := Real.zero_lt_one
-      _ ≤ x := hx.1
-    · calc x
-      _ ≤ π / 2 := hx.2
-      _ < π := div_two_lt_of_pos pi_pos
-  by_contra h₁x
-  simp at h₁x
-  rw [h₁x] at this
-  simp at this
-  exact one_le_pi_div_two
-
-lemma intervalIntegrable_log_sin : IntervalIntegrable (log ∘ sin) volume 0 π := by
-  apply IntervalIntegrable.trans (b := π / 2)
-  exact intervalIntegrable_log_sin₂
-  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
-  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
-  have : (fun x => log (cos x)) = log ∘ cos := rfl
-  apply IntervalIntegrable.symm
-  rwa [← this]
-
-
 theorem logInt
   {t : ℝ}
   (ht : 0 < t) :
@@ -281,108 +63,3 @@ theorem logInt
       exact (log_nonpos_iff hx.left).mpr hx.right.le
   · -- log is integrable on [[0, t]]
     simp [Set.mem_uIcc, ht]
-
-
-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 : ℝ} : 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
-
-  have t₂ {x : ℝ} : log (sin x) = log (sin (2 * x)) - log 2 - log (cos x) := by
-    rw [t₁]
-    ring
-
-  conv =>
-    left
-    arg 1
-    intro x
-    rw [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))]
-  simp
-  have : 2 * (π / 2) = π := by linarith
-  rw [this]
-
-  have : ∫ (x : ℝ) in (0)..π, log (sin x) = 2 * ∫ (x : ℝ) in (0)..(π / 2), log (sin x) := by
-    sorry
-  rw [this]
-  have : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) = ∫ (x : ℝ) in (0)..(π / 2), log (cos x) := by
-    sorry
-  rw [← this]
-  simp
-  linarith
-
-  exact Ne.symm (NeZero.ne' 2)
-  -- IntervalIntegrable (fun x => log (sin (2 * x))) volume 0 (π / 2)
-  sorry
-  -- 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
-  -- -- IntervalIntegrable (fun x => log 2) volume 0 (π / 2)
-  simp
-  -- -- IntervalIntegrable (fun x => log (cos x)) volume 0 (π / 2)
-  exact intervalIntegrable_log_cos
-
-
-lemma int₁₁ : ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) = 0 := by
-  sorry
-
-
-lemma int₁ :
-  ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - 1‖ = 0 := 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]
-      rw [Complex.normSq_apply]
-      simp
-    _ = sin x ^ 2 + cos x ^ 2 + 1 - 2 * cos x := by
-      ring
-    _ = 2 - 2 * cos x := by
-      rw [sin_sq_add_cos_sq]
-      norm_num
-    _ = 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]
-      ring
-    _ = 4 * sin (x / 2) ^ 2 := by
-      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
-  exact int₁₁
diff --git a/Nevanlinna/specialFunctions_Integral_log_sin.lean b/Nevanlinna/specialFunctions_Integral_log_sin.lean
index 92dcdc4..e4423a3 100644
--- a/Nevanlinna/specialFunctions_Integral_log_sin.lean
+++ b/Nevanlinna/specialFunctions_Integral_log_sin.lean
@@ -6,7 +6,6 @@ import Mathlib.MeasureTheory.Measure.Restrict
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
 
--- The following theorem was suggested by Gareth Ma on Zulip
 
 
 lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log ((π / 2)⁻¹ * x)‖ := by
@@ -227,62 +226,6 @@ lemma intervalIntegrable_log_cos : IntervalIntegrable (log ∘ cos) volume 0 (π
   rwa [← this]
 
 
-theorem logInt
-  {t : ℝ}
-  (ht : 0 < t) :
-  ∫ x in (0 : ℝ)..t, log x = t * log t - t := by
-  rw [← integral_add_adjacent_intervals (b := 1)]
-  trans (-1) + (t * log t - t + 1)
-  · congr
-    · -- ∫ x in 0..1, log x = -1, same proof as before
-      rw [integral_eq_sub_of_hasDerivAt_of_tendsto (f := fun x ↦ x * log x - x) (fa := 0) (fb := -1)]
-      · simp
-      · simp
-      · intro x hx
-        norm_num at hx
-        convert (hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x) using 1
-        norm_num
-      · rw [← neg_neg log]
-        apply IntervalIntegrable.neg
-        apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))
-        · exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg
-        · intro x hx
-          norm_num at hx
-          convert ((hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x)).neg using 1
-          norm_num
-        · intro x hx
-          norm_num at hx
-          rw [Pi.neg_apply, Left.nonneg_neg_iff]
-          exact (log_nonpos_iff hx.left).mpr hx.right.le
-      · have := tendsto_log_mul_rpow_nhds_zero zero_lt_one
-        simp_rw [rpow_one, mul_comm] at this
-        -- tendsto_nhdsWithin_of_tendsto_nhds should be under Tendsto namespace
-        convert this.sub (tendsto_nhdsWithin_of_tendsto_nhds tendsto_id)
-        norm_num
-      · rw [(by simp : -1 = 1 * log 1 - 1)]
-        apply tendsto_nhdsWithin_of_tendsto_nhds
-        exact (continuousAt_id.mul (continuousAt_log one_ne_zero)).sub continuousAt_id
-    · -- ∫ x in 1..t, log x = t * log t + 1, just use integral_log_of_pos
-      rw [integral_log_of_pos zero_lt_one ht]
-      norm_num
-  · abel
-  · -- log is integrable on [[0, 1]]
-    rw [← neg_neg log]
-    apply IntervalIntegrable.neg
-    apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))
-    · exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg
-    · intro x hx
-      norm_num at hx
-      convert ((hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x)).neg using 1
-      norm_num
-    · intro x hx
-      norm_num at hx
-      rw [Pi.neg_apply, Left.nonneg_neg_iff]
-      exact (log_nonpos_iff hx.left).mpr hx.right.le
-  · -- log is integrable on [[0, t]]
-    simp [Set.mem_uIcc, ht]
-
-
 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
@@ -333,56 +276,3 @@ lemma integral_log_sin : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) =  -log 2 *
   simp
   -- -- IntervalIntegrable (fun x => log (cos x)) volume 0 (π / 2)
   exact intervalIntegrable_log_cos
-
-
-lemma int₁₁ : ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) = 0 := by
-  sorry
-
-
-lemma int₁ :
-  ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - 1‖ = 0 := 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]
-      rw [Complex.normSq_apply]
-      simp
-    _ = sin x ^ 2 + cos x ^ 2 + 1 - 2 * cos x := by
-      ring
-    _ = 2 - 2 * cos x := by
-      rw [sin_sq_add_cos_sq]
-      norm_num
-    _ = 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]
-      ring
-    _ = 4 * sin (x / 2) ^ 2 := by
-      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
-  exact int₁₁
diff --git a/Nevanlinna/specialFunctions_Integrals.lean b/Nevanlinna/specialFunctions_Integrals.lean
deleted file mode 100644
index 92dcdc4..0000000
--- a/Nevanlinna/specialFunctions_Integrals.lean
+++ /dev/null
@@ -1,388 +0,0 @@
-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
-
--- The following theorem was suggested by Gareth Ma on Zulip
-
-
-lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log ((π / 2)⁻¹ * x)‖ := by
-
-  intro x hx
-  by_cases h'x : x = 0
-  · rw [h'x]; simp
-
-  -- Now handle the case where x ≠ 0
-  have l₀ : log ((π / 2)⁻¹ * x) ≤ 0 := by
-    apply log_nonpos
-    apply mul_nonneg
-    apply le_of_lt
-    apply inv_pos.2
-    apply div_pos
-    exact pi_pos
-    exact zero_lt_two
-    apply (Set.mem_Icc.1 hx).1
-    simp
-    apply mul_le_one
-    rw [div_le_one pi_pos]
-    exact two_le_pi
-    exact (Set.mem_Icc.1 hx).1
-    exact (Set.mem_Icc.1 hx).2
-
-  have l₁ : 0 ≤ sin x := by
-    apply sin_nonneg_of_nonneg_of_le_pi (Set.mem_Icc.1 hx).1
-    trans (1 : ℝ)
-    exact (Set.mem_Icc.1 hx).2
-    trans π / 2
-    exact one_le_pi_div_two
-    norm_num [pi_nonneg]
-  have l₂ : log (sin x) ≤ 0 := log_nonpos l₁ (sin_le_one x)
-
-  simp only [norm_eq_abs, Function.comp_apply]
-  rw [abs_eq_neg_self.2 l₀]
-  rw [abs_eq_neg_self.2 l₂]
-  simp only [neg_le_neg_iff, ge_iff_le]
-
-  have l₃ : x ∈ (Set.Ioi 0) := by
-    simp
-    exact lt_of_le_of_ne (Set.mem_Icc.1 hx).1 ( fun a => h'x (id (Eq.symm a)) )
-
-  have l₅ : 0 < (π / 2)⁻¹ * x := by
-    apply mul_pos
-    apply inv_pos.2
-    apply div_pos pi_pos zero_lt_two
-    exact l₃
-
-  have : ∀ x ∈ (Set.Icc 0 (π / 2)), (π / 2)⁻¹ * x ≤ sin x := by
-    intro x hx
-
-    have i₀ : 0 ∈ Set.Icc 0 π :=
-      Set.left_mem_Icc.mpr pi_nonneg
-    have i₁ : π / 2 ∈ Set.Icc 0 π :=
-      Set.mem_Icc.mpr ⟨div_nonneg pi_nonneg zero_le_two, half_le_self pi_nonneg⟩
-
-    have i₂ : 0 ≤ 1 - (π / 2)⁻¹ * x := by
-      rw [sub_nonneg]
-      calc (π / 2)⁻¹ * x
-      _ ≤ (π / 2)⁻¹ * (π / 2) := by
-        apply mul_le_mul_of_nonneg_left
-        exact (Set.mem_Icc.1 hx).2
-        apply inv_nonneg.mpr (div_nonneg pi_nonneg zero_le_two)
-      _ = 1 := by
-        apply inv_mul_cancel
-        apply div_ne_zero_iff.mpr
-        constructor
-        · exact pi_ne_zero
-        · exact Ne.symm (NeZero.ne' 2)
-
-    have i₃ : 0 ≤ (π / 2)⁻¹ * x := by
-      apply mul_nonneg
-      apply inv_nonneg.2
-      apply div_nonneg
-      exact pi_nonneg
-      exact zero_le_two
-      exact (Set.mem_Icc.1 hx).1
-
-    have i₄ : 1 - (π / 2)⁻¹ * x + (π / 2)⁻¹ * x = 1 := by ring
-
-    let B := strictConcaveOn_sin_Icc.concaveOn.2 i₀ i₁ i₂ i₃ i₄
-    simp [Real.sin_pi_div_two] at B
-    rw [(by ring_nf; rw [mul_inv_cancel pi_ne_zero, one_mul] : 2 / π * x * (π / 2) = x)] at B
-    simpa
-
-  apply log_le_log l₅
-  apply this
-  apply Set.mem_Icc.mpr
-  constructor
-  · exact le_of_lt l₃
-  · trans 1
-    exact (Set.mem_Icc.1 hx).2
-    exact one_le_pi_div_two
-
-
-lemma intervalIntegrable_log_sin₁ : IntervalIntegrable (log ∘ sin) volume 0 1 := by
-
-  have int_log : IntervalIntegrable (fun x ↦ ‖log x‖) volume 0 1 := by
-    apply IntervalIntegrable.norm
-    rw [← neg_neg log]
-    apply IntervalIntegrable.neg
-    apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))
-    · exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg
-    · intro x hx
-      norm_num at hx
-      convert ((hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x)).neg using 1
-      norm_num
-    · intro x hx
-      norm_num at hx
-      rw [Pi.neg_apply, Left.nonneg_neg_iff]
-      exact (log_nonpos_iff hx.left).mpr hx.right.le
-
-
-  have int_log : IntervalIntegrable (fun x ↦ ‖log ((π / 2)⁻¹ * x)‖) volume 0 1 := by
-
-    have A := IntervalIntegrable.comp_mul_right int_log (π / 2)⁻¹
-    simp only [norm_eq_abs] at A
-    conv =>
-      arg 1
-      intro x
-      rw [mul_comm]
-    simp only [norm_eq_abs]
-    apply IntervalIntegrable.mono A
-    simp
-    trans Set.Icc 0 (π / 2)
-    exact Set.Icc_subset_Icc (Preorder.le_refl 0) one_le_pi_div_two
-    exact Set.Icc_subset_uIcc
-    exact Preorder.le_refl volume
-
-  apply IntervalIntegrable.mono_fun' (g := fun x ↦ ‖log ((π / 2)⁻¹ * x)‖)
-  exact int_log
-
-  -- AEStronglyMeasurable (log ∘ sin) (volume.restrict (Ι 0 1))
-  apply ContinuousOn.aestronglyMeasurable
-  apply ContinuousOn.comp (t := Ι 0 1)
-  apply ContinuousOn.mono (s := {0}ᶜ)
-  exact continuousOn_log
-  intro x hx
-  by_contra contra
-  simp at contra
-  rw [contra, Set.left_mem_uIoc] at hx
-  linarith
-  exact continuousOn_sin
-
-  -- Set.MapsTo sin (Ι 0 1) (Ι 0 1)
-  rw [Set.uIoc_of_le (zero_le_one' ℝ)]
-  exact fun x hx ↦ ⟨sin_pos_of_pos_of_le_one hx.1 hx.2, sin_le_one x⟩
-
-  -- MeasurableSet (Ι 0 1)
-  exact measurableSet_uIoc
-
-  -- (fun x => ‖(log ∘ sin) x‖) ≤ᶠ[ae (volume.restrict (Ι 0 1))] ‖log‖
-  dsimp [EventuallyLE]
-  rw [MeasureTheory.ae_restrict_iff]
-  apply MeasureTheory.ae_of_all
-  intro x hx
-  have : x ∈ Set.Icc 0 1 := by
-    simp
-    simp at hx
-    constructor
-    · exact le_of_lt hx.1
-    · exact hx.2
-  let A := logsinBound x this
-  simp only [Function.comp_apply, norm_eq_abs] at A
-  exact A
-
-  apply measurableSet_le
-  apply Measurable.comp'
-  exact continuous_abs.measurable
-  exact Measurable.comp' measurable_log continuous_sin.measurable
-  -- Measurable fun a => |log ((π / 2)⁻¹ * a)|
-  apply Measurable.comp'
-  exact continuous_abs.measurable
-  apply Measurable.comp'
-  exact measurable_log
-  exact measurable_const_mul (π / 2)⁻¹
-
-lemma intervalIntegrable_log_sin₂ : IntervalIntegrable (log ∘ sin) volume 0 (π / 2) := by
-
-  apply IntervalIntegrable.trans (b := 1)
-  exact intervalIntegrable_log_sin₁
-
-  -- IntervalIntegrable (log ∘ sin) volume 1 (π / 2)
-  apply ContinuousOn.intervalIntegrable
-  apply ContinuousOn.comp continuousOn_log continuousOn_sin
-  intro x hx
-  rw [Set.uIcc_of_le, Set.mem_Icc] at hx
-  have : 0 < sin x := by
-    apply Real.sin_pos_of_pos_of_lt_pi
-    · calc 0
-      _ < 1 := Real.zero_lt_one
-      _ ≤ x := hx.1
-    · calc x
-      _ ≤ π / 2 := hx.2
-      _ < π := div_two_lt_of_pos pi_pos
-  by_contra h₁x
-  simp at h₁x
-  rw [h₁x] at this
-  simp at this
-  exact one_le_pi_div_two
-
-lemma intervalIntegrable_log_sin : IntervalIntegrable (log ∘ sin) volume 0 π := by
-  apply IntervalIntegrable.trans (b := π / 2)
-  exact intervalIntegrable_log_sin₂
-  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
-  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
-  have : (fun x => log (cos x)) = log ∘ cos := rfl
-  apply IntervalIntegrable.symm
-  rwa [← this]
-
-
-theorem logInt
-  {t : ℝ}
-  (ht : 0 < t) :
-  ∫ x in (0 : ℝ)..t, log x = t * log t - t := by
-  rw [← integral_add_adjacent_intervals (b := 1)]
-  trans (-1) + (t * log t - t + 1)
-  · congr
-    · -- ∫ x in 0..1, log x = -1, same proof as before
-      rw [integral_eq_sub_of_hasDerivAt_of_tendsto (f := fun x ↦ x * log x - x) (fa := 0) (fb := -1)]
-      · simp
-      · simp
-      · intro x hx
-        norm_num at hx
-        convert (hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x) using 1
-        norm_num
-      · rw [← neg_neg log]
-        apply IntervalIntegrable.neg
-        apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))
-        · exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg
-        · intro x hx
-          norm_num at hx
-          convert ((hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x)).neg using 1
-          norm_num
-        · intro x hx
-          norm_num at hx
-          rw [Pi.neg_apply, Left.nonneg_neg_iff]
-          exact (log_nonpos_iff hx.left).mpr hx.right.le
-      · have := tendsto_log_mul_rpow_nhds_zero zero_lt_one
-        simp_rw [rpow_one, mul_comm] at this
-        -- tendsto_nhdsWithin_of_tendsto_nhds should be under Tendsto namespace
-        convert this.sub (tendsto_nhdsWithin_of_tendsto_nhds tendsto_id)
-        norm_num
-      · rw [(by simp : -1 = 1 * log 1 - 1)]
-        apply tendsto_nhdsWithin_of_tendsto_nhds
-        exact (continuousAt_id.mul (continuousAt_log one_ne_zero)).sub continuousAt_id
-    · -- ∫ x in 1..t, log x = t * log t + 1, just use integral_log_of_pos
-      rw [integral_log_of_pos zero_lt_one ht]
-      norm_num
-  · abel
-  · -- log is integrable on [[0, 1]]
-    rw [← neg_neg log]
-    apply IntervalIntegrable.neg
-    apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))
-    · exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg
-    · intro x hx
-      norm_num at hx
-      convert ((hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x)).neg using 1
-      norm_num
-    · intro x hx
-      norm_num at hx
-      rw [Pi.neg_apply, Left.nonneg_neg_iff]
-      exact (log_nonpos_iff hx.left).mpr hx.right.le
-  · -- log is integrable on [[0, t]]
-    simp [Set.mem_uIcc, ht]
-
-
-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 : ℝ} : 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
-
-  have t₂ {x : ℝ} : log (sin x) = log (sin (2 * x)) - log 2 - log (cos x) := by
-    rw [t₁]
-    ring
-
-  conv =>
-    left
-    arg 1
-    intro x
-    rw [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))]
-  simp
-  have : 2 * (π / 2) = π := by linarith
-  rw [this]
-
-  have : ∫ (x : ℝ) in (0)..π, log (sin x) = 2 * ∫ (x : ℝ) in (0)..(π / 2), log (sin x) := by
-    sorry
-  rw [this]
-  have : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) = ∫ (x : ℝ) in (0)..(π / 2), log (cos x) := by
-    sorry
-  rw [← this]
-  simp
-  linarith
-
-  exact Ne.symm (NeZero.ne' 2)
-  -- IntervalIntegrable (fun x => log (sin (2 * x))) volume 0 (π / 2)
-  sorry
-  -- 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
-  -- -- IntervalIntegrable (fun x => log 2) volume 0 (π / 2)
-  simp
-  -- -- IntervalIntegrable (fun x => log (cos x)) volume 0 (π / 2)
-  exact intervalIntegrable_log_cos
-
-
-lemma int₁₁ : ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) = 0 := by
-  sorry
-
-
-lemma int₁ :
-  ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - 1‖ = 0 := 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]
-      rw [Complex.normSq_apply]
-      simp
-    _ = sin x ^ 2 + cos x ^ 2 + 1 - 2 * cos x := by
-      ring
-    _ = 2 - 2 * cos x := by
-      rw [sin_sq_add_cos_sq]
-      norm_num
-    _ = 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]
-      ring
-    _ = 4 * sin (x / 2) ^ 2 := by
-      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
-  exact int₁₁