From 5cdc786144e0dec3c2dc911543a0b3f1a329be04 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 6 Nov 2024 15:33:48 +0100
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/divisor.lean      | 34 ++++++++++++++++++++++++++++++++++
 Nevanlinna/mathlibAddOn.lean | 21 +++++++++++++++++++++
 2 files changed, 55 insertions(+)

diff --git a/Nevanlinna/divisor.lean b/Nevanlinna/divisor.lean
index 72e0bff..aa3c5d4 100644
--- a/Nevanlinna/divisor.lean
+++ b/Nevanlinna/divisor.lean
@@ -2,6 +2,7 @@ import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
 import Mathlib.Analysis.Convex.SpecificFunctions.Deriv
 import Nevanlinna.analyticAt
+import Nevanlinna.mathlibAddOn
 
 open Interval Topology
 open Real Filter MeasureTheory intervalIntegral
@@ -20,3 +21,36 @@ instance
   coe := Divisor.toFun
 
 attribute [coe] Divisor.toFun
+
+
+theorem Divisor.closedSupport
+  {U : Set ℂ}
+  (hU : IsClosed U)
+  (D : Divisor U) :
+  IsClosed D.toFun.support := by
+
+  rw [← isOpen_compl_iff]
+  rw [isOpen_iff_eventually]
+  intro x hx
+  by_cases h₁x : x ∈ U
+  · have A := D.locallyFiniteInU x h₁x
+    simp [A]
+    simp at hx
+    let B := Mnhds A hx
+    simpa
+  · rw [eventually_iff_exists_mem]
+    use Uᶜ
+    constructor
+    · exact IsClosed.compl_mem_nhds hU h₁x
+    · intro y hy
+      simp
+      exact Function.nmem_support.mp fun a => hy (D.supportInU a)
+
+
+theorem Divisor.finiteSupport
+  {U : Set ℂ}
+  (hU : IsCompact U)
+  (D : Divisor U) :
+  Set.Finite D.toFun.support := by
+
+  sorry
diff --git a/Nevanlinna/mathlibAddOn.lean b/Nevanlinna/mathlibAddOn.lean
index 7fec19b..e5957f6 100644
--- a/Nevanlinna/mathlibAddOn.lean
+++ b/Nevanlinna/mathlibAddOn.lean
@@ -1,6 +1,7 @@
 import Mathlib.Analysis.Analytic.Meromorphic
 import Mathlib.Analysis.Calculus.ContDiff.Basic
 import Mathlib.Analysis.Calculus.FDeriv.Add
+import Nevanlinna.analyticAt
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
@@ -51,3 +52,23 @@ theorem meromorphicAt_congr'
   {f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜}
   (h : f =ᶠ[nhds x] g) : MeromorphicAt f x ↔ MeromorphicAt g x :=
   meromorphicAt_congr (Filter.EventuallyEq.filter_mono h nhdsWithin_le_nhds)
+
+open Topology Filter
+
+lemma Mnhds
+  {α : Type}
+  {f g : ℂ → α}
+  {z₀ : ℂ}
+  (h₁ : f =ᶠ[𝓝[≠] z₀] g)
+  (h₂ : f z₀ = g z₀) :
+  f =ᶠ[𝓝 z₀] g := by
+  apply eventually_nhds_iff.2
+  obtain ⟨t, h₁t, h₂t⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₁)
+  use t
+  constructor
+  · intro y hy
+    by_cases h₂y : y ∈ ({z₀}ᶜ : Set ℂ)
+    · exact h₁t y hy h₂y
+    · simp at h₂y
+      rwa [h₂y]
+  · exact h₂t