kebekus
/
nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update stronglyMeromorphic.lean

This commit is contained in:
Stefan Kebekus 2024-10-24 13:12:03 +02:00
parent 570a58aab7
commit 6aa5bc3b1c
1 changed files with 13 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
Nevanlinna/stronglyMeromorphic.lean
View File

@ -134,6 +134,15 @@ lemma Mnhds
· exact h₂t · exact h₂t
theorem localIdentity
{f g : ℂ → ℂ}
{z₀ : ℂ}
(hf : AnalyticAt ℂ f z₀)
(hg : AnalyticAt ℂ g z₀) :
f =ᶠ[𝓝[≠] z₀] g → f =ᶠ[𝓝 z₀] g := by
sorry
theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
{f : ℂ → ℂ} {f : ℂ → ℂ}
{z₀ : ℂ} {z₀ : ℂ}
@ -174,12 +183,13 @@ theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
simp [h₃f] simp [h₃f]
obtain ⟨h₁G, h₂G, h₃G⟩ := Classical.choose_spec h₄f obtain ⟨h₁G, h₂G, h₃G⟩ := Classical.choose_spec h₄f
simp at h₃G simp at h₃G
have hn : n = 0 := by have hn : n = 0 := Eq.symm ((fun {α} {a} {b} h => (WithTop.eq_untop_iff h).mpr) h₂f (id (Eq.symm h₃f)))
sorry
rw [hn] rw [hn]
rw [hn] at h₃g; simp at h₃g
simp simp
have : g =ᶠ[𝓝 z₀] G := by have : g =ᶠ[𝓝 z₀] G := by
sorry apply localIdentity h₁g h₁G
exact Filter.EventuallyEq.trans (Filter.EventuallyEq.symm h₃g) h₃G
rw [Filter.EventuallyEq.eq_of_nhds this] rw [Filter.EventuallyEq.eq_of_nhds this]
· have : hf.order ≠ 0 := h₃f · have : hf.order ≠ 0 := h₃f
simp [this] simp [this]