nevanlinna/Nevanlinna/logabs.lean

import Mathlib.Analysis.Complex.CauchyIntegral
open ComplexConjugate

/- logAbs of a product is sum of logAbs of factors -/

lemma logAbs_mul : ∀ z₁ z₂ : ℂ, z₁ ≠ 0 → z₂ ≠ 0 → Real.log (Complex.abs (z₁ * z₂)) = Real.log (Complex.abs z₁) + Real.log (Complex.abs z₂) := by
  intro z₁ z₂ z₁Hyp z₂Hyp
  rw [Complex.instNormedFieldComplex.proof_2 z₁ z₂]
  exact Real.log_mul ((AbsoluteValue.ne_zero_iff Complex.abs).mpr z₁Hyp) ((AbsoluteValue.ne_zero_iff Complex.abs).mpr z₂Hyp)

lemma absAndProd : ∀ z : ℂ, Complex.abs z = Real.sqrt ( (z * conj z).re ) := by
  intro z
  simp
  rfl

#check Complex.log_mul_eq_add_log_iff
#check Complex.arg_eq_pi_iff

lemma logAbsXX : ∀ z : ℂ, z ≠ 0 → Real.log (Complex.abs z) = (1 / 2) * Complex.log z + (1 / 2) * Complex.log (conj z) := by
  intro z z₁Hyp

  by_cases argHyp : Complex.arg z = Real.pi

  -- Show pos: Complex.arg z = Real.pi
  have : conj z = z := by
    apply Complex.conj_eq_iff_im.2
    rw [Complex.arg_eq_pi_iff] at argHyp
    exact argHyp.right
  rw [this]
  sorry

  -- Show pos: Complex.arg z ≠ Real.pi
  have t₁ : Complex.abs z = Real.sqrt (Complex.normSq z) := by
    exact rfl
  rw [t₁]
  
  have t₂ : 0 ≤ Complex.normSq z := by
    exact Complex.normSq_nonneg z
  rw [ Real.log_sqrt t₂ ]


  have t₃ : Real.log (Complex.normSq z) = Complex.log (Complex.normSq z) := by
    apply Complex.ofReal_log
    exact t₂
  simp
  rw [t₃]
  rw [Complex.normSq_eq_conj_mul_self]
  
  have t₄ : conj z ≠ 0 := by
    exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr z₁Hyp

  let XX := Complex.log_mul_eq_add_log_iff this z₁Hyp



  sorry