kebekus/nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Working

Browse Source
This commit is contained in:
Stefan Kebekus 2024-11-28 18:24:08 +01:00
parent 8bc84748a3
commit 2b7ab1af9d
1 changed files with 11 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean
View File

@ -63,6 +63,13 @@ theorem stronglyMeromorphicOn_ratlPolynomial₃
apply analyticOnNhd_const apply analyticOnNhd_const
theorem stronglyMeromorphicOn_ratlPolynomial₃U
(d : ℂ → ℤ)
(U : Set ℂ) :
StronglyMeromorphicOn (∏ᶠ u, fun z ↦ (z - u) ^ d u) U := by
intro z hz
exact stronglyMeromorphicOn_ratlPolynomial₃ d z (trivial)
theorem stronglyMeromorphicOn_divisor_ratlPolynomial₁ theorem stronglyMeromorphicOn_divisor_ratlPolynomial₁
{z : ℂ} {z : ℂ}
@ -166,7 +173,10 @@ theorem stronglyMeromorphicOn_ratlPolynomial₃order
have : (Function.mulSupport fun u z => (z - u) ^ d u).Infinite := by have : (Function.mulSupport fun u z => (z - u) ^ d u).Infinite := by
exact hd exact hd
simp_rw [finprod_of_infinite_mulSupport this] simp_rw [finprod_of_infinite_mulSupport this]
sorry have : AnalyticAt ℂ (1 : ℂ → ℂ) z := by exact analyticAt_const
rw [AnalyticAt.meromorphicAt_order this]
rw [this.order_eq_zero_iff.2 (by simp)]
simp
theorem stronglyMeromorphicOn_divisor_ratlPolynomial theorem stronglyMeromorphicOn_divisor_ratlPolynomial