Working…

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

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

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 : ℂ}

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