From 24bd4f9ffa3a91e20f4fd628b280c06c8bc1ef49 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 13 Nov 2024 16:12:25 +0100
Subject: [PATCH] =?UTF-8?q?Working=E2=80=A6?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Nevanlinna/analyticAt.lean              | 14 ++++++++++++++
 Nevanlinna/meromorphicOn_decompose.lean |  4 +++-
 2 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/Nevanlinna/analyticAt.lean b/Nevanlinna/analyticAt.lean
index afa3c8d..22831aa 100644
--- a/Nevanlinna/analyticAt.lean
+++ b/Nevanlinna/analyticAt.lean
@@ -266,3 +266,17 @@ theorem AnalyticAt.mul₁
   AnalyticAt ℂ (f * g) z := by
   rw [(by rfl : f * g = (fun x ↦ f x * g x))]
   exact mul hf hg
+
+
+theorem analyticAt_finprod
+  {α : Type}
+  {f : α → ℂ → ℂ}
+  {z : ℂ}
+  (hf : ∀ a, AnalyticAt ℂ (f a) z) :
+  AnalyticAt ℂ (∏ᶠ a, f a) z := by
+  by_cases h₁f : (Function.mulSupport f).Finite
+  · rw [finprod_eq_prod f h₁f]
+    rw [Finset.prod_fn h₁f.toFinset f]
+    exact Finset.analyticAt_prod h₁f.toFinset (fun a _ ↦ hf a)
+  · rw [finprod_of_infinite_mulSupport h₁f]
+    exact analyticAt_const
diff --git a/Nevanlinna/meromorphicOn_decompose.lean b/Nevanlinna/meromorphicOn_decompose.lean
index a35a670..b7a85d1 100644
--- a/Nevanlinna/meromorphicOn_decompose.lean
+++ b/Nevanlinna/meromorphicOn_decompose.lean
@@ -71,7 +71,9 @@ theorem MeromorphicOn.decompose
         use (∏ᶠ p ≠ z, (fun x ↦ (x - p) ^ h₁f.divisor p)) * g
         constructor
         · apply AnalyticAt.mul₁
-          ·
+          · apply analyticAt_finprod
+            intro w
+
             sorry
           · apply (h₃g z hz).analytic
             rw [h₂g ⟨z, hz⟩]