From 025b0a3db8c89570d05e3d73038c4a325d696d58 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 31 Oct 2024 17:09:09 +0100
Subject: [PATCH] Create meromorphicOn_divisor.lean

---
 Nevanlinna/meromorphicOn_divisor.lean | 61 +++++++++++++++++++++++++++
 1 file changed, 61 insertions(+)
 create mode 100644 Nevanlinna/meromorphicOn_divisor.lean

diff --git a/Nevanlinna/meromorphicOn_divisor.lean b/Nevanlinna/meromorphicOn_divisor.lean
new file mode 100644
index 0000000..80b12b7
--- /dev/null
+++ b/Nevanlinna/meromorphicOn_divisor.lean
@@ -0,0 +1,61 @@
+import Mathlib.Analysis.Analytic.Meromorphic
+import Nevanlinna.analyticAt
+import Nevanlinna.divisor
+
+
+open scoped Interval Topology
+open Real Filter MeasureTheory intervalIntegral
+
+
+noncomputable def MeromorphicOn.divisor
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hf : MeromorphicOn f U) :
+  Divisor U where
+
+  toFun := by
+    intro z
+    if hz : z ∈ U then
+      exact ((hf z hz).order.untop' 0 : ℤ)
+    else
+      exact 0
+
+  supportInU := by
+    intro z hz
+    simp at hz
+    by_contra h₂z
+    simp [h₂z] at hz
+
+  locallyFiniteInU := by
+    intro z hz
+
+    apply eventually_nhdsWithin_iff.2
+    rw [eventually_nhds_iff]
+
+    rcases AnalyticAt.eventually_eq_zero_or_eventually_ne_zero (hf z hz) with h|h
+    · rw [eventually_nhds_iff] at h
+      obtain ⟨N, h₁N, h₂N, h₃N⟩ := h
+      use N
+      constructor
+      · intro y h₁y _
+        by_cases h₃y : y ∈ U
+        · simp [h₃y]
+          right
+          rw [AnalyticAt.order_eq_top_iff (hf y h₃y)]
+          rw [eventually_nhds_iff]
+          use N
+        · simp [h₃y]
+      · tauto
+
+    · rw [eventually_nhdsWithin_iff, eventually_nhds_iff] at h
+      obtain ⟨N, h₁N, h₂N, h₃N⟩ := h
+      use N
+      constructor
+      · intro y h₁y h₂y
+        by_cases h₃y : y ∈ U
+        · simp [h₃y]
+          left
+          rw [AnalyticAt.order_eq_zero_iff (hf y h₃y)]
+          exact h₁N y h₁y h₂y
+        · simp [h₃y]
+      · tauto