From 4320db0533290c9f398c4d0144eb601243b66408 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 2 Dec 2024 16:49:16 +0100
Subject: [PATCH] Update stronglyMeromorphic_JensenFormula.lean

---
 .../stronglyMeromorphic_JensenFormula.lean    | 62 +++++++++++++------
 1 file changed, 42 insertions(+), 20 deletions(-)

diff --git a/Nevanlinna/stronglyMeromorphic_JensenFormula.lean b/Nevanlinna/stronglyMeromorphic_JensenFormula.lean
index 4b0fded..803b68f 100644
--- a/Nevanlinna/stronglyMeromorphic_JensenFormula.lean
+++ b/Nevanlinna/stronglyMeromorphic_JensenFormula.lean
@@ -29,34 +29,56 @@ theorem jensen_case_R_eq_one
   have h'₂f : ∃ u : (Metric.closedBall (0 : ℂ) 1), f u ≠ 0 := by
     use ⟨0, Metric.mem_closedBall_self (by simp)⟩
 
+  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: Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log (‖s‖⁻¹)) ⊆ h₃f.toFinset := by
+    intro x
+    contrapose
+    simp
+    intro hx
+    rw [hx]
+    simp
+  rw [finsum_eq_sum_of_support_subset _ h₄f]
+
   obtain ⟨F, h₁F, h₂F, h₃F, h₄F⟩ := MeromorphicOn.decompose₃' h₂U h₁U h₁f h'₂f
 
-  let G := fun z ↦ log ‖F z‖ + ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order s).toNat * log ‖z - s‖
+  have h₁F : Function.mulSupport (fun u ↦ fun z => (z - u) ^ (h₁f.meromorphicOn.divisor u)) ⊆ h₃f.toFinset := by
+    intro u
+    contrapose
+    simp
+    intro hu
+    rw [hu]
+    simp
+    exact rfl
+  rw [finprod_eq_prod_of_mulSupport_subset _ h₁F] at h₄F
+
+  let G := fun z ↦ log ‖F z‖ + ∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log ‖z - s‖
+
+  have h₁G {z : ℂ} : Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log ‖z - s‖) ⊆ h₃f.toFinset := by
+    intro s
+    contrapose
+    simp
+    intro hs
+    rw [hs]
+    simp
 
   have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → log ‖f z‖ = G z := by
     intro z h₁z h₂z
 
-    conv =>
-      left
-      arg 1
-      rw [h₃F]
-      rw [smul_eq_mul]
-      rw [norm_mul]
-      rw [norm_prod]
-      left
-      arg 2
-      intro b
-      rw [norm_pow]
-    simp only [Complex.norm_eq_abs, Finset.univ_eq_attach]
+    rw [h₄F]
+    simp only [Pi.mul_apply, norm_mul]
+    simp only [Finset.prod_apply, norm_prod, norm_zpow]
     rw [Real.log_mul]
     rw [Real.log_prod]
-    conv =>
-      left
-      left
-      arg 2
-      intro s
-      rw [Real.log_pow]
-    dsimp [G]
+    simp_rw [Real.log_zpow]
+    dsimp only [G]
+    rw [finsum_eq_sum_of_support_subset _ h₁G]
+    --
+    intro x hx
+    simp at hx
+
+
     abel
 
     -- ∀ x ∈ ⋯.toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0