Working…

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

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⟩]