Update mathlib

Nevanlinna/analyticOnNhd_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.divisor
 
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
@@ -9,89 +10,24 @@ open Real Filter MeasureTheory intervalIntegral
 
 
 
-structure Divisor where
-  toFun : ℂ → ℤ
-  -- This is not what we want. We want: locally finite
-  discreteSupport : DiscreteTopology (Function.support toFun)
-
-instance : CoeFun Divisor (fun _ ↦ ℂ → ℤ) where
-coe := Divisor.toFun
-attribute [coe] Divisor.toFun
-
-
-
-noncomputable def Divisor.deg
-  (D : Divisor) : ℤ := ∑ᶠ z, D z
-
-noncomputable def Divisor.n_trunk
-  (D : Divisor) : ℤ → ℝ → ℤ := fun k r ↦ ∑ᶠ z ∈ Metric.ball 0 r, min k (D z)
-
-noncomputable def Divisor.n
-  (D : Divisor) : ℝ → ℤ := fun r ↦ ∑ᶠ z ∈ Metric.ball 0 r, D z
-
-noncomputable def Divisor.N_trunk
-  (D : Divisor) : ℤ → ℝ → ℝ := fun k r ↦ ∫ (t : ℝ) in (1)..r, (D.n_trunk k t) / t
-
-
-theorem Divisor.support_cap_closed₁
-  {S U : Set ℂ}
-  (hS : DiscreteTopology S)
-  (hU : IsClosed U) :
-  IsClosed (U ∩ S) := by
-
-  rw [← isOpen_compl_iff]
-  rw [isOpen_iff_forall_mem_open]
-  intro x hx
-  by_cases h₁x : x ∈ U
-  · simp at hx
-
-
-    sorry
-  · use Uᶜ
-    constructor
-    · simp
-    · constructor
-      · exact IsClosed.isOpen_compl
-      · assumption
-
-
-
-theorem Divisor.support_cap_closed
-  (D : Divisor)
-  {U : Set ℂ}
-  (h₁U : IsClosed U) :
-  IsClosed (U ∩ D.toFun.support) := by
-  sorry
-
-
-theorem Divisor.support_cap_compact
-  (D : Divisor)
-  {U : Set ℂ}
-  (h₁U : IsCompact U) :
-  Set.Finite (U ∩ (Function.support D)) := by
-
-  apply IsCompact.finite
-  -- Target set is compact
-  apply h₁U.of_isClosed_subset
-  apply D.support_cap_closed h₁U.isClosed
-  exact Set.inter_subset_left
-  -- Target set is discrete
-  apply DiscreteTopology.of_subset D.discreteSupport
-  exact Set.inter_subset_right
-
-
 noncomputable def AnalyticOnNhd.zeroDivisor
   {f : ℂ → ℂ}
   {U : Set ℂ}
   (hf : AnalyticOnNhd ℂ f U) :
-  Divisor where
+  Divisor U where
+
+  toFun := by
+    intro z
+    if hz : z ∈ U then
+      exact ((hf z hz).order.toNat : ℤ)
+    else
+      exact 0
+
+  supportInU := by
+    intro z hz
+    simp only [Function.mem_support] at hz
+    simp only [Function.mem_support, ne_eq, dite_eq_else, Nat.cast_eq_zero, ENat.toNat_eq_zero, not_forall, not_or] at hz
 
-    toFun := by
-      intro z
-      if hz : z ∈ U then
-        exact ((hf z hz).order.toNat : ℤ)
-      else
-        exact 0
 
     discreteSupport := by
       simp_rw [← singletons_open_iff_discrete]

Nevanlinna/holomorphic_JensenFormula.lean

@@ -1,6 +1,6 @@
 import Mathlib.Analysis.Complex.CauchyIntegral
 import Mathlib.Analysis.Analytic.IsolatedZeros
-import Nevanlinna.analyticOn_zeroSet
+import Nevanlinna.analyticOnNhd_zeroSet
 import Nevanlinna.harmonicAt_examples
 import Nevanlinna.harmonicAt_meanValue
 import Nevanlinna.specialFunctions_CircleIntegral_affine

Nevanlinna/holomorphic_primitive.lean

@@ -666,7 +666,7 @@ theorem primitive_additivity'
       dsimp [ε']; simp
       have : |ε| = ε := by apply abs_of_pos h₁ε
       rw [this]
-      apply (inv_mul_lt_iff zero_lt_two).mpr
+      apply (inv_mul_lt_iff₀ zero_lt_two).mpr
       linarith
     have h₁ε' : 0 < ε' := by
       apply mul_pos _ h₁ε

Nevanlinna/holomorphic_zero.lean

@@ -3,7 +3,7 @@ import Mathlib.Analysis.Analytic.Meromorphic
 import Mathlib.Topology.ContinuousOn
 import Mathlib.Analysis.Analytic.IsolatedZeros
 import Nevanlinna.holomorphic
-import Nevanlinna.analyticOn_zeroSet
+import Nevanlinna.analyticOnNhd_zeroSet
 
 
 noncomputable def zeroDivisor