22 lines
643 B
Plaintext
22 lines
643 B
Plaintext
|
import Mathlib.Analysis.Analytic.Meromorphic
|
|||
|
|
import Nevanlinna.analyticAt
|
|||
|
|
|
|||
|
|
def StronglyMeromorphicAt
|
|||
|
|
(f : ℂ → ℂ)
|
|||
|
|
(z₀ : ℂ) :=
|
|||
|
|
(∀ᶠ (z : ℂ) in nhds z₀, f z = 0) ∨ (∃ (n : ℕ), ∃ g : ℂ → ℂ, (AnalyticAt ℂ g z₀) ∧ (g z₀ ≠ 0) ∧ (∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ n • g z))
|
|||
|
|
|
|||
|
|
def MeromorphicAt.makeStronglyMeromorphic
|
|||
|
|
{f : ℂ → ℂ}
|
|||
|
|
{z₀ : ℂ}
|
|||
|
|
(hf : MeromorphicAt f z₀) :
|
|||
|
|
ℂ → ℂ := by
|
|||
|
|
exact 0
|
|||
|
|
|
|||
|
|
theorem makeStronglyMeromorphic
|
|||
|
|
{f : ℂ → ℂ}
|
|||
|
|
{z₀ : ℂ}
|
|||
|
|
(hf : MeromorphicAt f z₀) :
|
|||
|
|
StronglyMeromorphicAt hf.makeStronglyMeromorphic z₀ := by
|
|||
|
|
sorry
|