nevanlinna/Nevanlinna/firstMain.lean

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

open Real


-- Lang p. 164
noncomputable def MeromorphicOn.N_zero
  {f : ℂ → ℂ}
  (h₁f : MeromorphicOn f ⊤) :
  ℝ → ℝ :=
  fun r ↦ ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, (max 0 (h₁f.divisor z)) * log (r * ‖z‖⁻¹)

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

theorem Nevanlinna_counting
  {f : ℂ → ℂ}
  (h₁f : MeromorphicOn f ⊤) :
  h₁f.N_zero - h₁f.N_infty = fun r ↦ ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, (h₁f.divisor z) * log (r * ‖z‖⁻¹) := by
  sorry

--

noncomputable def logpos : ℝ → ℝ :=
  fun r ↦ max 0 (log r)

theorem loglogpos
  {r : ℝ} :
  log r = logpos r - logpos r⁻¹ := by
  unfold logpos
  rw [log_inv]
  by_cases h : 0 ≤ log r
  · simp [h]
  · simp at h
    have : 0 ≤ -log r := Left.nonneg_neg_iff.2 (le_of_lt h)
    simp [h, this]
    exact neg_nonneg.mp this

--

noncomputable def MeromorphicOn.m_infty
  {f : ℂ → ℂ}
  (h₁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)))
  --
  sorry

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
  funext r
  simp
  unfold MeromorphicOn.T_infty
  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