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 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.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 ⊤) (hr : 0 < r) : (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 hr intro z hx exact h₁f z trivial -- apply MeromorphicOn.integrable_logpos_abs_f hr exact MeromorphicOn.inv_iff.mpr fun x a => h₁f x trivial 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 by_cases h₁r : r = 0 · unfold MeromorphicOn.m_infty rw [← mul_sub]; congr simp only [h₁r, circleMap_zero_radius, Function.const_apply, intervalIntegral.integral_const, sub_zero, smul_eq_mul, Pi.inv_apply, norm_inv] rw [← mul_sub]; congr exact loglogpos by_cases h₂r : 0 < r · exact Nevanlinna_proximity₀ h₁f h₂r 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 sorry 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