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

Update meromorphicOn_decompose.lean

This commit is contained in:
Stefan Kebekus 2024-11-08 12:05:49 +01:00
parent 4145a9ebc9
commit 6d403874e2
1 changed files with 8 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
Nevanlinna/meromorphicOn_decompose.lean
View File

@ -36,11 +36,15 @@ theorem MeromorphicOn.decompose
∧ (Set.EqOn h₁f.makeStronglyMeromorphicOn (fun z ↦ ∏ᶠ p, (z - p) ^ (h₁f.divisor p) * g z ) U) := by ∧ (Set.EqOn h₁f.makeStronglyMeromorphicOn (fun z ↦ ∏ᶠ p, (z - p) ^ (h₁f.divisor p) * g z ) U) := by
let g₁ : ℂ → ℂ := f * (fun z ↦ ∏ᶠ p, (z - p) ^ (h₁f.divisor p)) let g₁ : ℂ → ℂ := f * (fun z ↦ ∏ᶠ p, (z - p) ^ (h₁f.divisor p))
have h₁g₁ : MeromorphicOn g₁ U := by sorry have h₁g₁ : MeromorphicOn g₁ U := by
sorry
let g := h₁g₁.makeStronglyMeromorphicOn let g := h₁g₁.makeStronglyMeromorphicOn
have h₁g : MeromorphicOn g U := by sorry have h₁g : MeromorphicOn g U := by
have h₂g : ∀ z : U, (h₁g z.1 z.2).order = 0 := by sorry sorry
have h₃g : StronglyMeromorphicOn g U := by sorry have h₂g : ∀ z : U, (h₁g z.1 z.2).order = 0 := by
sorry
have h₃g : StronglyMeromorphicOn g U := by
sorry
have h₄g : AnalyticOnNhd ℂ g U := by have h₄g : AnalyticOnNhd ℂ g U := by
intro z hz intro z hz
apply StronglyMeromorphicAt.analytic (h₃g z hz) apply StronglyMeromorphicAt.analytic (h₃g z hz)
@ -51,10 +55,8 @@ theorem MeromorphicOn.decompose
· constructor · constructor
· intro z hz · intro z hz
rw [← (h₄g z hz).order_eq_zero_iff] rw [← (h₄g z hz).order_eq_zero_iff]
have A := (h₄g z hz).meromorphicAt_order have A := (h₄g z hz).meromorphicAt_order
rw [h₂g ⟨z, hz⟩] at A rw [h₂g ⟨z, hz⟩] at A
have t₀ : (h₄g z hz).order ≠ ⊤ := by have t₀ : (h₄g z hz).order ≠ ⊤ := by
by_contra hC by_contra hC
rw [hC] at A rw [hC] at A