Nevanlinna/divisor.lean

@@ -2,7 +2,6 @@ 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
@@ -21,73 +20,3 @@ 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,7 +1,6 @@
 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]
@@ -52,23 +51,3 @@ 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