diff --git a/Nevanlinna/meromorphicOn_decompose.lean b/Nevanlinna/meromorphicOn_decompose.lean index ceb2ba4..a13c472 100644 --- a/Nevanlinna/meromorphicOn_decompose.lean +++ b/Nevanlinna/meromorphicOn_decompose.lean @@ -19,5 +19,28 @@ theorem MeromorphicOn.decompose (h₂f : ∃ z₀ ∈ U, f z₀ ≠ 0) : ∃ g : ℂ → ℂ, (AnalyticOnNhd ℂ g U) ∧ (∀ z ∈ U, g z ≠ 0) - ∧ (Set.EqOn h₁f.makeStronglyMeromorphicOn (fun z ↦ ∏ᶠ p ∈ h₁f.divisor.support, (z-p) ) U) := by - sorry + ∧ (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 + 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 : AnalyticOnNhd ℂ g U := by + intro z hz + apply StronglyMeromorphicAt.analytic (h₃g z hz) + rw [h₂g ⟨z, hz⟩] + use g + constructor + · exact h₄g + · constructor + · intro z hz + rw [← (h₄g z hz).order_eq_zero_iff] + + let A := (h₄g z hz).meromorphicAt_order + let B := h₂g ⟨z, hz⟩ + sorry + · intro z hz + + sorry