Create meromorphicOn_divisor.lean

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