Update stronglyMeromorphic_JensenFormula.lean

Nevanlinna/stronglyMeromorphic_JensenFormula.lean

@@ -149,11 +149,32 @@ theorem jensen_case_R_eq_one
 
   have decompose_int_G : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x)
     = (∫ (x : ℝ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 1 x))))
-        + ∑ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order x).toNat * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by
+        + ∑ᶠ x, (h₁f.meromorphicOn.divisor x) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by
     dsimp [G]
+
     rw [intervalIntegral.integral_add]
+    congr
+    have t₀ {x : ℝ} : Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log (Complex.abs (circleMap 0 1 x - s))) ⊆ h₃f.toFinset := by
+      intro s hs
+      simp at hs
+      simp [hs.1]
+    conv =>
+      left
+      arg 1
+      intro x
+      rw [finsum_eq_sum_of_support_subset _ t₀]
     rw [intervalIntegral.integral_finset_sum]
-    simp_rw [intervalIntegral.integral_const_mul]
+    let G' := fun x ↦ ((h₁f.meromorphicOn.divisor x) : ℂ) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - x))
+    have t₁ : (Function.support fun x ↦ (h₁f.meromorphicOn.divisor x) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - x))) ⊆ h₃f.toFinset := by
+      simp
+      intro s
+      contrapose!
+      simp
+      tauto
+    conv =>
+      right
+      rw [finsum_eq_sum_of_support_subset _ t₁]
+    simp
 
     --  ∀ i ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset,
     --  IntervalIntegrable (fun x => (h'₁f.order i).toNat *
@@ -161,7 +182,7 @@ theorem jensen_case_R_eq_one
     intro i _
     apply IntervalIntegrable.const_mul
     --simp at this
-    by_cases h₂i : ‖i.1‖ = 1
+    by_cases h₂i : ‖i‖ = 1
     -- case pos
     exact int'₂ h₂i
     -- case neg
@@ -195,7 +216,9 @@ theorem jensen_case_R_eq_one
     rw [this]
     apply ContinuousAt.comp
     apply Real.continuousAt_log
-    simp [h₂F]
+    simp
+    exact h₃F ⟨(circleMap 0 1 x), (by simp)⟩
+
     -- ContinuousAt (⇑Complex.abs ∘ F ∘ fun x => circleMap 0 1 x) x
     apply ContinuousAt.comp
     apply Complex.continuous_abs.continuousAt