57 lines
1.2 KiB
Lean4
57 lines
1.2 KiB
Lean4
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
|
||
|
||
|
||
structure Divisor
|
||
(U : Set ℂ)
|
||
where
|
||
toFun : ℂ → ℤ
|
||
supportInU : toFun.support ⊆ U
|
||
locallyFiniteInU : ∀ x ∈ U, toFun =ᶠ[𝓝[≠] x] 0
|
||
|
||
instance
|
||
(U : Set ℂ) :
|
||
CoeFun (Divisor U) (fun _ ↦ ℂ → ℤ) where
|
||
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
|