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

Update stronglyMeromorphicAt.lean

This commit is contained in:
Stefan Kebekus 2024-11-14 15:32:19 +01:00
parent 1a14bbbdd6
commit 9ebb1c5215
1 changed files with 41 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
Nevanlinna/stronglyMeromorphicAt.lean
View File

@ -399,6 +399,44 @@ theorem StronglyMeromorphicAt.decompose
· rw [h₂g] · rw [h₂g]
· exact h₁g · exact h₁g
· constructor · constructor
· exact (order_eq_zero_iff h₁g).mp h₂g · rwa [← h₁g.order_eq_zero_iff]
· · funext z
sorry by_cases hz : z = z₀
· by_cases hOrd : h₁f.meromorphicAt.order.untop h₂f = 0
· simp [hOrd]
have : StronglyMeromorphicAt g₁ z₀ := by
unfold g₁
simp [hOrd]
have : (fun z => 1) * f = f := by
funext z
simp
rwa [this]
rw [hz]
unfold g
let A := makeStronglyMeromorphic_id this
rw [← A]
unfold g₁
rw [hOrd]
simp
· have : h₁f.meromorphicAt.order ≠ 0 := by
by_contra hC
simp_rw [hC] at hOrd
tauto
let A := h₁f.order_eq_zero_iff.not.1 this
simp at A
rw [hz, A]
simp
left
rw [zpow_eq_zero_iff]
assumption
· simp
have : g z = g₁ z := by
exact Eq.symm (m₁ h₁g₁ z hz)
rw [this]
unfold g₁
simp [hz]
rw [← mul_assoc]
rw [mul_inv_cancel₀]
simp
apply zpow_ne_zero
exact sub_ne_zero_of_ne hz