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

Update stronglyMeromorphicOn_eliminate.lean

Browse Source
This commit is contained in:
Stefan Kebekus 2024-11-27 10:43:13 +01:00
parent 37359a319f
commit 9be57a898c
1 changed files with 11 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
Nevanlinna/stronglyMeromorphicOn_eliminate.lean
View File

@ -367,26 +367,25 @@ theorem MeromorphicOn.decompose₃'
have h₄f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := h₁f.meromorphicOn.divisor.finiteSupport h₁U
let d := - h₁f.meromorphicOn.divisor.toFun
have h₁d : d.support = (Function.support h₁f.meromorphicOn.divisor) := by
ext x
unfold d
simp
let h₁ := ∏ᶠ u, fun z ↦ (z - u) ^ (d u)
have h₁h₁ : StronglyMeromorphicOn h₁ U := by
intro z hz
exact stronglyMeromorphicOn_ratlPolynomial₃ d z trivial
have h₂h₁ : h₁h₁.meromorphicOn.divisor = d := by
sorry
have h₃h₁ : ∀ (z : ℂ) (hz : z ∈ U), (h₁h₁ z hz).meromorphicAt.order ≠ ⊤ := by
sorry
let g' := f * h₁
have h₁g' : MeromorphicOn g' U := h₁f.meromorphicOn.mul h₁h₁.meromorphicOn
have h₂g' : h₁g'.divisor.toFun = 0 := by
rw [MeromorphicOn.divisor_mul h₁f.meromorphicOn (fun z hz ↦ h₃f ⟨z, hz⟩) h₁h₁.meromorphicOn _]
unfold MeromorphicOn.divisor
rw [MeromorphicOn.divisor_mul h₁f.meromorphicOn (fun z hz ↦ h₃f ⟨z, hz⟩) h₁h₁.meromorphicOn h₃h₁]
rw [h₂h₁]
unfold d
simp
funext z
by_cases hz : z ∈ U
· simp [hz]
have : (Function.support d).Finite := by
sorry
rw [stronglyMeromorphicOn_divisor_ratlPolynomial₁ d this]
simp
sorry
· simp [hz]
sorry
let g := h₁g'.makeStronglyMeromorphicOn
have h₁g : StronglyMeromorphicOn g U := by