nevanlinna/Nevanlinna/specialFunctions_Integral_log_sin.lean

import Mathlib.Analysis.SpecialFunctions.Integrals
import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

open scoped Interval Topology
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

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

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
  have : (fun x => log (cos x)) = log ∘ cos := rfl
  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)..π, log (sin x) = 2 * ∫ (x : ℝ) in (0)..(π / 2), log (sin x) := by
  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]


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
    simp at hx

    rw [sin_two_mul x, log_mul, log_mul]
    exact Ne.symm (NeZero.ne' 2)
    -- 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₂ : 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

  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))]
  simp
  have : 2 * (π / 2) = π := by linarith
  rw [this]
  rw [integral_log_sin₀]

  have : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) = ∫ (x : ℝ) in (0)..(π / 2), log (cos x) := by
    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)
  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)
  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]


lemma integral_log_sin₂ : ∫ (x : ℝ) in (0)..π, log (sin x) = -log 2 * π := by
  rw [integral_log_sin₀, integral_log_sin₁]
  ring