nevanlinna/Nevanlinna/specialFunctions_Integrals.lean

import Mathlib.Analysis.SpecialFunctions.Integrals
import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
import Mathlib.MeasureTheory.Integral.CircleIntegral

open scoped Interval Topology
open Real Filter MeasureTheory intervalIntegral

-- The following theorem was suggested by Gareth Ma on Zulip

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 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



  sorry