70 lines
1.8 KiB
Plaintext
70 lines
1.8 KiB
Plaintext
import Mathlib.Analysis.Analytic.Meromorphic
|
||
import Nevanlinna.analyticAt
|
||
|
||
|
||
/- Strongly MeromorphicAt -/
|
||
|
||
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))
|
||
|
||
|
||
/- Strongly MeromorphicAt is Meromorphic -/
|
||
theorem StronglyMeromorphicAt.meromorphicAt
|
||
{f : ℂ → ℂ}
|
||
{z₀ : ℂ}
|
||
(hf : StronglyMeromorphicAt f z₀) :
|
||
MeromorphicAt f z₀ := by
|
||
rcases hf with h|h
|
||
· use 0; simp
|
||
rw [analyticAt_congr h]
|
||
exact analyticAt_const
|
||
· obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h
|
||
have : MeromorphicAt (fun z ↦ (z - z₀) ^ n • g z) z₀ := by
|
||
simp
|
||
apply MeromorphicAt.mul
|
||
apply MeromorphicAt.zpow
|
||
apply MeromorphicAt.sub
|
||
|
||
sorry
|
||
apply MeromorphicAt.congr this
|
||
rw [Filter.eventuallyEq_comm]
|
||
exact Filter.EventuallyEq.filter_mono h₃g nhdsWithin_le_nhds
|
||
|
||
/- Strongly MeromorphicAt of positive order is analytic -/
|
||
theorem StronglyMeromorphicAt.analytic
|
||
{f : ℂ → ℂ}
|
||
{z₀ : ℂ}
|
||
(h₁f : StronglyMeromorphicAt f z₀)
|
||
(h₂f : 0 ≤ h₁f.meromorphicAt.order):
|
||
AnalyticAt ℂ f z₀ := by
|
||
sorry
|
||
|
||
|
||
|
||
/- Make strongly MeromorphicAt -/
|
||
|
||
def MeromorphicAt.makeStronglyMeromorphicAt
|
||
{f : ℂ → ℂ}
|
||
{z₀ : ℂ}
|
||
(hf : MeromorphicAt f z₀) :
|
||
ℂ → ℂ := by
|
||
exact 0
|
||
|
||
|
||
theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
|
||
{f : ℂ → ℂ}
|
||
{z₀ : ℂ}
|
||
(hf : MeromorphicAt f z₀) :
|
||
StronglyMeromorphicAt hf.makeStronglyMeromorphic z₀ := by
|
||
sorry
|
||
|
||
|
||
theorem makeStronglyMeromorphic_eventuallyEq
|
||
{f : ℂ → ℂ}
|
||
{z₀ : ℂ}
|
||
(hf : MeromorphicAt f z₀) :
|
||
∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = hf.makeStronglyMeromorphicAt z := by
|
||
sorry
|