nevanlinna/Nevanlinna/divisor.lean

import Mathlib.Analysis.SpecialFunctions.Integrals
import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
import Mathlib.Analysis.Convex.SpecificFunctions.Deriv
import Nevanlinna.analyticAt

open Interval Topology
open Real Filter MeasureTheory intervalIntegral


structure Divisor
  (U : Set ℂ)
  where
  toFun : ℂ → ℤ
  supportInU : toFun.support ⊆ U
  locallyFiniteInU : ∀ x ∈ U, ∃  N ∈ 𝓝 x, (N ∩ toFun.support).Finite

instance
  (U : Set ℂ) :
  CoeFun (Divisor U) (fun _ ↦ ℂ → ℤ) where
  coe := Divisor.toFun

attribute [coe] Divisor.toFun