diff --git a/Nevanlinna/stronglyMeromorphic.lean b/Nevanlinna/stronglyMeromorphic.lean new file mode 100644 index 0000000..6f3f4a9 --- /dev/null +++ b/Nevanlinna/stronglyMeromorphic.lean @@ -0,0 +1,21 @@ +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