From cf301d65d60f63de2345607e40f1e675b746f59d Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 16 Dec 2024 07:36:01 +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                         | 16 +++++++++++++++-
 Nevanlinna/meromorphicOn_divisor.lean           | 15 +++++++++++++++
 Nevanlinna/meromorphicOn_integrability.lean     |  2 ++
 Nevanlinna/stronglyMeromorphicOn_eliminate.lean |  3 ++-
 4 files changed, 34 insertions(+), 2 deletions(-)

diff --git a/Nevanlinna/divisor.lean b/Nevanlinna/divisor.lean
index 8e74b25..3bc52e5 100644
--- a/Nevanlinna/divisor.lean
+++ b/Nevanlinna/divisor.lean
@@ -23,6 +23,7 @@ instance
 attribute [coe] Divisor.toFun
 
 
+
 theorem Divisor.discreteSupport
   {U : Set ℂ}
   (hU : IsClosed U)
@@ -57,7 +58,6 @@ theorem Divisor.discreteSupport
         exact False.elim (h₁x (A x hx))
 
 
-
 theorem Divisor.closedSupport
   {U : Set ℂ}
   (hU : IsClosed U)
@@ -91,3 +91,17 @@ theorem Divisor.finiteSupport
   · apply IsCompact.of_isClosed_subset hU (D.closedSupport hU.isClosed)
     exact D.supportInU
   · exact D.discreteSupport hU.isClosed
+
+
+theorem Divisor.codiscreteWithin
+  {U : Set ℂ}
+  (D : Divisor U) :
+  D.toFun.supportᶜ ∈ Filter.codiscreteWithin U := by
+
+  simp_rw [mem_codiscreteWithin, disjoint_principal_right]
+  intro x hx
+  obtain ⟨s, hs⟩ := Filter.eventuallyEq_iff_exists_mem.1 (D.locallyFiniteInU x hx)
+  apply Filter.mem_of_superset hs.1
+  intro y hy
+  simp [hy]
+  tauto
diff --git a/Nevanlinna/meromorphicOn_divisor.lean b/Nevanlinna/meromorphicOn_divisor.lean
index 2e7ba1b..793392e 100644
--- a/Nevanlinna/meromorphicOn_divisor.lean
+++ b/Nevanlinna/meromorphicOn_divisor.lean
@@ -182,3 +182,18 @@ theorem StronglyMeromorphicOn.analyticOnNhd
     tauto
     tauto
   assumption
+
+theorem StronglyMeromorphicOn.support_divisor
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hU : IsPreconnected U)
+  (h₁f : StronglyMeromorphicOn f U)
+  (h₂f : ∃ u ∈ U, f u ≠ 0) :
+  U ∩ f⁻¹' {0} = (Function.support h₁f.meromorphicOn.divisor) := by
+
+  ext u
+  constructor
+  · sorry
+  · intro hu
+    simp at hu
+    sorry
diff --git a/Nevanlinna/meromorphicOn_integrability.lean b/Nevanlinna/meromorphicOn_integrability.lean
index 4d07d91..0be7e59 100644
--- a/Nevanlinna/meromorphicOn_integrability.lean
+++ b/Nevanlinna/meromorphicOn_integrability.lean
@@ -12,6 +12,8 @@ open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
 
 
+/- Integral and Integrability up to changes on codiscrete sets -/
+
 theorem d
   {U S : Set ℂ}
   {c : ℂ}
diff --git a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
index cb895e3..7b29890 100644
--- a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
+++ b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
@@ -529,7 +529,8 @@ theorem MeromorphicOn.decompose_log
   rw [Filter.eventuallyEq_iff_exists_mem]
   use {z | f z ≠ 0}
   constructor
-  · sorry
+  ·
+    sorry
   · intro z hz
     nth_rw 1 [h₄g]
     simp