Update stronglyMeromorphic_JensenFormula.lean

Nevanlinna/stronglyMeromorphic_JensenFormula.lean

@@ -1,12 +1,5 @@
-import Mathlib.Analysis.Complex.CauchyIntegral
-import Mathlib.Analysis.Analytic.IsolatedZeros
-import Nevanlinna.analyticOnNhd_zeroSet
-import Nevanlinna.harmonicAt_examples
-import Nevanlinna.harmonicAt_meanValue
 import Nevanlinna.specialFunctions_CircleIntegral_affine
-import Nevanlinna.stronglyMeromorphicOn
 import Nevanlinna.stronglyMeromorphicOn_eliminate
-import Nevanlinna.meromorphicOn_divisor
 
 open Real
 
@@ -31,9 +24,30 @@ theorem jensen
   have h'₂f : ∃ u : (Metric.closedBall (0 : ℂ) R), f u ≠ 0 := by
     use ⟨0, Metric.mem_closedBall_self (le_of_lt hR)⟩
 
+  have h'₁f : StronglyMeromorphicAt f 0 := by
+    apply h₁f
+    simp
+    exact le_of_lt hR
+
+  have h''₂f : h'₁f.meromorphicAt.order = 0 := by
+    rwa [h'₁f.order_eq_zero_iff]
+
+  have h'''₂f : h₁f.meromorphicOn.divisor 0 = 0 := by
+    unfold MeromorphicOn.divisor
+    simp
+    tauto
+
   have h₃f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := by
     exact Divisor.finiteSupport h₂U (StronglyMeromorphicOn.meromorphicOn h₁f).divisor
 
+  have h'₃f : ∀ s ∈ h₃f.toFinset, s ≠ 0 := by
+    by_contra hCon
+    push_neg at hCon
+    obtain ⟨s, h₁s, h₂s⟩ := hCon
+    rw [h₂s] at h₁s
+    simp at h₁s
+    tauto
+
   have h₄f: Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log (R * ‖s‖⁻¹)) ⊆ h₃f.toFinset := by
     intro x
     contrapose
@@ -147,7 +161,7 @@ theorem jensen
     apply Set.Finite.countable
     exact Finset.finite_toSet h₃f.toFinset
     --
-    simp
+    exact Ne.symm (ne_of_lt hR)
 
 
   have decompose_int_G : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 R x)
@@ -359,39 +373,31 @@ theorem jensen
   rw [mul_add]
   ring
   --
-
+  exact Ne.symm (ne_of_lt hR)
-
-  --
-  intro x hx
-  simp at hx
-  rw [zpow_ne_zero_iff]
-  by_contra hCon
-  simp at hCon
-  rw [← (h₁f 0 (by simp)).order_eq_zero_iff] at h₂f
-  rw [hCon] at hx
-  unfold MeromorphicOn.divisor at hx
-  simp at hx
-  rw [h₂f] at hx
-  tauto
-  assumption
   --
   simp
-
   by_contra hCon
-  nth_rw 1 [h₄F] at h₂f
+  rw [hCon] at hs
-  simp at h₂f
+  simp at hs
-  tauto
+  exact hs h'''₂f
+  --
+  intro s hs
+  apply zpow_ne_zero
+  simp
+  by_contra hCon
+  rw [hCon] at hs
+  simp at hs
+  exact hs h'''₂f
+  --
+  simp only [ne_eq, map_eq_zero]
+  rw [← ne_eq]
+  exact h₃F ⟨0, (by simp; exact le_of_lt hR)⟩
   --
   rw [Finset.prod_ne_zero_iff]
-  intro x hx
+  intro s hs
-  simp at hx
+  apply zpow_ne_zero
-  rw [zpow_ne_zero_iff]
+  simp
   by_contra hCon
-  simp at hCon
+  rw [hCon] at hs
-  rw [← (h₁f 0 (by simp)).order_eq_zero_iff] at h₂f
+  simp at hs
-  rw [hCon] at hx
+  exact hs h'''₂f
-  unfold MeromorphicOn.divisor at hx
-  simp at hx
-  rw [h₂f] at hx
-  tauto
-  assumption