Update divisor.lean

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,73 @@ instance
   coe := Divisor.toFun
 
 attribute [coe] Divisor.toFun
+
+
+theorem Divisor.discreteSupport
+  {U : Set ℂ}
+  (hU : IsClosed U)
+  (D : Divisor U) :
+  DiscreteTopology D.toFun.support := by
+  apply discreteTopology_subtype_iff.mpr
+  intro x hx
+  apply inf_principal_eq_bot.mpr
+  by_cases h₁x : x ∈ U
+  · let A := D.locallyFiniteInU x h₁x
+    refine mem_nhdsWithin.mpr ?_
+    rw [eventuallyEq_nhdsWithin_iff] at A
+    obtain ⟨U, h₁U, h₂U, h₃U⟩ := eventually_nhds_iff.1 A
+    use U
+    constructor
+    · exact h₂U
+    · constructor
+      · exact h₃U
+      · intro y hy
+        let C := h₁U y hy.1 hy.2
+        tauto
+  · refine mem_nhdsWithin.mpr ?_
+    use Uᶜ
+    constructor
+    · simpa
+    · constructor
+      · tauto
+      · intro y _
+        let A := D.supportInU
+        simp at A
+        simp
+        exact False.elim (h₁x (A x hx))
+
+
+
+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
+  apply IsCompact.finite
+  · apply IsCompact.of_isClosed_subset hU (D.closedSupport hU.isClosed)
+    exact D.supportInU
+  · exact D.discreteSupport hU.isClosed

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