nevanlinna/Nevanlinna/firstMain.lean

import Mathlib.MeasureTheory.Integral.CircleIntegral
import Nevanlinna.divisor
import Nevanlinna.stronglyMeromorphicOn
import Nevanlinna.meromorphicOn_divisor
import Nevanlinna.meromorphicOn_integrability

open Real


-- Lang p. 164

theorem MeromorphicOn.restrict
  {f : ℂ → ℂ}
  (h₁f : MeromorphicOn f ⊤)
  (r : ℝ) :
  MeromorphicOn f (Metric.closedBall 0 r) := by
  exact fun x a => h₁f x trivial

theorem MeromorphicOn.restrict_inv
  {f : ℂ → ℂ}
  (h₁f : MeromorphicOn f ⊤)
  (r : ℝ) :
  h₁f.inv.restrict r = (h₁f.restrict r).inv := by
  funext x
  simp


noncomputable def MeromorphicOn.N_zero
  {f : ℂ → ℂ}
  (hf : MeromorphicOn f ⊤) :
  ℝ → ℝ :=
  fun r ↦ ∑ᶠ z, (max 0 ((hf.restrict r).divisor z)) * log (r * ‖z‖⁻¹)

noncomputable def MeromorphicOn.N_infty
  {f : ℂ → ℂ}
  (hf : MeromorphicOn f ⊤) :
  ℝ → ℝ :=
  fun r ↦ ∑ᶠ z, (max 0 (-((hf.restrict r).divisor z))) * log (r * ‖z‖⁻¹)

theorem Nevanlinna_counting₀
  {f : ℂ → ℂ}
  (hf : MeromorphicOn f ⊤) :
  hf.inv.N_infty = hf.N_zero := by
  funext r
  unfold MeromorphicOn.N_zero MeromorphicOn.N_infty
  let A := (hf.restrict r).divisor.finiteSupport (isCompact_closedBall 0 r)
  repeat
    rw [finsum_eq_sum_of_support_subset (s := A.toFinset)]
  apply Finset.sum_congr rfl
  intro x hx
  congr
  rw [hf.restrict_inv r]
  rw [MeromorphicOn.divisor_inv]
  simp
  --
  exact fun x a => hf x trivial
  --
  intro x
  contrapose
  simp
  intro hx
  rw [hx]
  tauto
  --
  intro x
  contrapose
  simp
  intro hx h₁x
  rw [hf.restrict_inv r] at h₁x
  have hh : MeromorphicOn f (Metric.closedBall 0 r) := hf.restrict r
  rw [hh.divisor_inv] at h₁x
  simp at h₁x
  rw [hx] at h₁x
  tauto


theorem Nevanlinna_counting
  {f : ℂ → ℂ}
  (hf : MeromorphicOn f ⊤) :
  hf.N_zero - hf.N_infty = fun r ↦ ∑ᶠ z, ((hf.restrict r).divisor z) * log (r * ‖z‖⁻¹) := by

  funext r
  simp only [Pi.sub_apply]
  unfold  MeromorphicOn.N_zero MeromorphicOn.N_infty

  let A := (hf.restrict r).divisor.finiteSupport (isCompact_closedBall 0 r)
  repeat
    rw [finsum_eq_sum_of_support_subset (s := A.toFinset)]
  rw [← Finset.sum_sub_distrib]
  simp_rw [← sub_mul]
  congr
  funext x
  congr
  by_cases h : 0 ≤ (hf.restrict r).divisor x
  · simp [h]
  · have h' : 0 ≤ -((hf.restrict r).divisor x) := by
      simp at h
      apply Int.le_neg_of_le_neg
      simp
      exact Int.le_of_lt h
    simp at h
    simp [h']
    linarith
  --
  repeat
    intro x
    contrapose
    simp
    intro hx
    rw [hx]
    tauto


--

noncomputable def MeromorphicOn.m_infty
  {f : ℂ → ℂ}
  (_ : MeromorphicOn f ⊤) :
  ℝ → ℝ :=
  fun r ↦ (2 * π)⁻¹ * ∫ x in (0)..(2 * π), logpos ‖f (circleMap 0 r x)‖


theorem Nevanlinna_proximity
  {f : ℂ → ℂ}
  {r : ℝ}
  (h₁f : MeromorphicOn f ⊤) :
  (2 * π)⁻¹ * ∫ x in (0)..(2 * π), log ‖f (circleMap 0 r x)‖ = (h₁f.m_infty r) - (h₁f.inv.m_infty r) := by

  unfold MeromorphicOn.m_infty
  rw [← mul_sub]; congr
  rw [← intervalIntegral.integral_sub]; congr
  funext x
  simp_rw [loglogpos]; congr
  exact Eq.symm (IsAbsoluteValue.abv_inv Norm.norm (f (circleMap 0 r x)))
  --
  apply MeromorphicOn.integrable_logpos_abs_f
  intro z hx
  exact h₁f z trivial
  --
  apply MeromorphicOn.integrable_logpos_abs_f
  exact MeromorphicOn.inv_iff.mpr fun x a => h₁f x trivial


noncomputable def MeromorphicOn.T_infty
  {f : ℂ → ℂ}
  (hf : MeromorphicOn f ⊤) :
  ℝ → ℝ :=
  hf.m_infty + hf.N_infty


theorem Nevanlinna_firstMain₁
  {f : ℂ → ℂ}
  (h₁f : MeromorphicOn f ⊤)
  (h₂f : StronglyMeromorphicAt f 0)
  (h₃f : f 0 ≠ 0) :
  (fun r ↦ log ‖f 0‖) + h₁f.inv.T_infty = h₁f.T_infty := by

  rw [add_eq_of_eq_sub]
  unfold MeromorphicOn.T_infty

  have {A B C D : ℝ → ℝ} : A + B - (C + D) = A - C + (B - D) := by
    ring
  rw [this]
  clear this

  funext r
  simp
  rw [← Nevanlinna_proximity h₁f]



  unfold MeromorphicOn.N_infty
  unfold MeromorphicOn.m_infty
  simp
  sorry

theorem Nevanlinna_firstMain₂
  {f : ℂ → ℂ}
  {a : ℂ}
  {r : ℝ}
  (h₁f : MeromorphicOn f ⊤) :
  |(h₁f.T_infty r) - ((h₁f.sub (MeromorphicOn.const a)).T_infty r)| ≤ logpos ‖a‖ + log 2 := by
  sorry