From 6d403874e2b8473bc75dcb057293b10783443aa1 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Fri, 8 Nov 2024 12:05:49 +0100 Subject: [PATCH] Update meromorphicOn_decompose.lean --- Nevanlinna/meromorphicOn_decompose.lean | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/Nevanlinna/meromorphicOn_decompose.lean b/Nevanlinna/meromorphicOn_decompose.lean index b0bba43..e9a0b0b 100644 --- a/Nevanlinna/meromorphicOn_decompose.lean +++ b/Nevanlinna/meromorphicOn_decompose.lean @@ -36,11 +36,15 @@ theorem MeromorphicOn.decompose ∧ (Set.EqOn h₁f.makeStronglyMeromorphicOn (fun z ↦ ∏ᶠ p, (z - p) ^ (h₁f.divisor p) * g z ) U) := by let g₁ : ℂ → ℂ := f * (fun z ↦ ∏ᶠ p, (z - p) ^ (h₁f.divisor p)) - have h₁g₁ : MeromorphicOn g₁ U := by sorry + have h₁g₁ : MeromorphicOn g₁ U := by + sorry let g := h₁g₁.makeStronglyMeromorphicOn - have h₁g : MeromorphicOn g U := by sorry - have h₂g : ∀ z : U, (h₁g z.1 z.2).order = 0 := by sorry - have h₃g : StronglyMeromorphicOn g U := by sorry + have h₁g : MeromorphicOn g U := by + sorry + have h₂g : ∀ z : U, (h₁g z.1 z.2).order = 0 := by + sorry + have h₃g : StronglyMeromorphicOn g U := by + sorry have h₄g : AnalyticOnNhd ℂ g U := by intro z hz apply StronglyMeromorphicAt.analytic (h₃g z hz) @@ -51,10 +55,8 @@ theorem MeromorphicOn.decompose · constructor · intro z hz rw [← (h₄g z hz).order_eq_zero_iff] - have A := (h₄g z hz).meromorphicAt_order rw [h₂g ⟨z, hz⟩] at A - have t₀ : (h₄g z hz).order ≠ ⊤ := by by_contra hC rw [hC] at A