From 12f0543f4764f3b3f2e20390e95df3a2feb96181 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Sat, 14 Sep 2024 08:38:04 +0200
Subject: [PATCH] =?UTF-8?q?Working=E2=80=A6?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Nevanlinna/analyticAt.lean |  12 ++++
 Nevanlinna/divisor.lean    | 129 +++++++++++++++++++++++++++++++++++++
 Nevanlinna/firstMain.lean  |  14 ++--
 3 files changed, 150 insertions(+), 5 deletions(-)
 create mode 100644 Nevanlinna/divisor.lean

diff --git a/Nevanlinna/analyticAt.lean b/Nevanlinna/analyticAt.lean
index afbb8da..807c463 100644
--- a/Nevanlinna/analyticAt.lean
+++ b/Nevanlinna/analyticAt.lean
@@ -3,6 +3,18 @@ import Mathlib.Analysis.Complex.Basic
 import Mathlib.Analysis.Analytic.Linear
 
 
+theorem AnalyticAt.order_neq_top_iff
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : AnalyticAt ℂ f z₀) :
+  hf.order ≠ ⊤ ↔ ∃ (g : ℂ → ℂ), AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ (hf.order.toNat) • g z := by
+  rw [← hf.order_eq_nat_iff]
+  constructor
+  · intro h₁f
+    exact Eq.symm (ENat.coe_toNat h₁f)
+  · intro h₁f
+    exact ENat.coe_toNat_eq_self.mp (id (Eq.symm h₁f))
+
 
 theorem AnalyticAt.order_mul
   {f₁ f₂ : ℂ → ℂ}
diff --git a/Nevanlinna/divisor.lean b/Nevanlinna/divisor.lean
new file mode 100644
index 0000000..3f86e6c
--- /dev/null
+++ b/Nevanlinna/divisor.lean
@@ -0,0 +1,129 @@
+import Nevanlinna.analyticAt
+
+
+structure Divisor where
+  toFun : ℂ → ℤ
+  discreteSupport : DiscreteTopology (Function.support toFun)
+
+instance : CoeFun Divisor (fun _ ↦ ℂ → ℤ) where
+coe := Divisor.toFun
+attribute [coe] Divisor.toFun
+
+
+
+noncomputable def Divisor.deg
+  (D : Divisor) : ℤ := ∑ᶠ z, D z
+
+noncomputable def Divisor.n_trunk
+  (D : Divisor) : ℤ → ℝ → ℤ := fun k r ↦ ∑ᶠ z ∈ Metric.ball 0 r, min k (D z)
+
+noncomputable def Divisor.n
+  (D : Divisor) : ℝ → ℤ := fun r ↦ ∑ᶠ z ∈ Metric.ball 0 r, D z
+
+noncomputable def Divisor.N_trunk
+  (D : Divisor) : ℤ → ℝ → ℝ := fun k r ↦ ∫ (t : ℝ) in (1)..r, (D.n_trunk k t) / t
+
+
+
+
+noncomputable def AnalyticOn.zeroDivisor
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hf : AnalyticOn ℂ f U) :
+  Divisor where
+
+    toFun := by
+      intro z
+      if hz : z ∈ U then
+        exact ((hf z hz).order.toNat : ℤ)
+      else
+        exact 0
+
+    discreteSupport := by
+      simp_rw [← singletons_open_iff_discrete]
+      simp_rw [Metric.isOpen_singleton_iff]
+      simp
+
+      --  simp only [dite_eq_ite, gt_iff_lt, Subtype.forall, Function.mem_support, ne_eq, ite_eq_else, Classical.not_imp, not_or, Subtype.mk.injEq]
+
+      intro a ha ⟨h₁a, h₂a⟩
+      obtain ⟨g, h₁g, h₂g, h₃g⟩ := (AnalyticAt.order_neq_top_iff (hf a ha)).1 h₂a
+      rw [Metric.eventually_nhds_iff_ball] at h₃g
+
+      have : ∃ ε > 0, ∀ y ∈ Metric.ball (↑a) ε, g y ≠ 0 := by
+        have h₄g : ContinuousAt g a :=
+          AnalyticAt.continuousAt h₁g
+        have : {0}ᶜ ∈ nhds (g a) := by
+          exact compl_singleton_mem_nhds_iff.mpr h₂g
+        let F := h₄g.preimage_mem_nhds this
+        rw [Metric.mem_nhds_iff] at F
+        obtain ⟨ε, h₁ε, h₂ε⟩ := F
+        use ε
+        constructor; exact h₁ε
+        intro y hy
+        let G := h₂ε hy
+        simp at G
+        exact G
+
+      obtain ⟨ε₁, h₁ε₁⟩ := this
+      obtain ⟨ε₂, h₁ε₂, h₂ε₂⟩ := h₃g
+      use min ε₁ ε₂
+      constructor
+      · have : 0 < min ε₁ ε₂ := by
+          rw [lt_min_iff]
+          exact And.imp_right (fun _ => h₁ε₂) h₁ε₁
+        exact this
+
+      intro y hy ⟨h₁y, h₂y⟩ h₃
+
+      have h'₂y : ↑y ∈ Metric.ball (↑a) ε₂ := by
+        simp
+        calc dist y a
+        _ < min ε₁ ε₂ := by assumption
+        _ ≤ ε₂ := by exact min_le_right ε₁ ε₂
+
+      have h₃y : ↑y ∈ Metric.ball (↑a) ε₁ := by
+        simp
+        calc dist y a
+        _ < min ε₁ ε₂ := by assumption
+        _ ≤ ε₁ := by exact min_le_left ε₁ ε₂
+
+      have F := h₂ε₂ y h'₂y
+      have : f y = 0 := by
+        rw [AnalyticAt.order_eq_zero_iff (hf y hy)] at h₁y
+        tauto
+      rw [this] at F
+      simp at F
+
+      have : g y ≠ 0 := by
+        exact h₁ε₁.2 y h₃y
+      simp [this] at F
+      rw [sub_eq_zero] at F
+      tauto
+
+
+theorem AnalyticOn.support_of_zeroDivisor
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hf : AnalyticOn ℂ f U) :
+  Function.support hf.zeroDivisor ⊆ U := by
+
+  intro z
+  contrapose
+  intro hz
+  dsimp [AnalyticOn.zeroDivisor]
+  simp
+  tauto
+
+
+theorem AnalyticOn.support_of_zeroDivisor₂
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hf : AnalyticOn ℂ f U) :
+  Function.support hf.zeroDivisor ⊆ f⁻¹' {0} := by
+
+  simp
+  intro z hz
+  dsimp [AnalyticOn.zeroDivisor]
+  simp
+  tauto
diff --git a/Nevanlinna/firstMain.lean b/Nevanlinna/firstMain.lean
index 0bdc7d4..f4b4e9a 100644
--- a/Nevanlinna/firstMain.lean
+++ b/Nevanlinna/firstMain.lean
@@ -1,15 +1,19 @@
+import Mathlib.Analysis.Analytic.Meromorphic
 import Nevanlinna.holomorphic_JensenFormula
 
 open Real
 
-variable {f : ℂ → ℂ}
-variable {h₁f : AnalyticOn ℂ f ⊤}
+variable (f : ℂ → ℂ)
+variable {h₁f : MeromorphicOn f ⊤}
 variable {h₂f : f 0 ≠ 0}
 
-noncomputable def unintegratedCounting : ℝ → ℕ := by
+
+
+noncomputable def Nevanlinna.n : ℝ → ℤ := by
   intro r
-  let A := h₁f.mono (by tauto : Metric.closedBall (0 : ℂ) r ⊆ ⊤)
-  exact ∑ᶠ z, (A.order z).toNat
+  have : MeromorphicAt f z := by
+    exact h₁f (sorryAx ℂ true) trivial
+  exact ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, (h₁f z trivial).order
 
 noncomputable def integratedCounting : ℝ → ℝ := by
   intro r