Compare commits

...

2 Commits

Author SHA1 Message Date
Stefan Kebekus fb642a4ed0 working 2024-11-14 16:18:32 +01:00
Stefan Kebekus f22cea20a0 Update stronglyMeromorphicAt.lean 2024-11-14 15:54:21 +01:00
2 changed files with 12 additions and 3 deletions

View File

@ -10,6 +10,17 @@ import Nevanlinna.mathlibAddOn
open scoped Interval Topology
open Real Filter MeasureTheory intervalIntegral
theorem MeromorphicOn.order_ne_top
{f : }
{U : Set }
(h₁U : IsConnected U)
(h₂U : IsCompact U)
(h₁f : MeromorphicOn f U)
(h₂f : ∃ z₀ ∈ U, f z₀ ≠ 0) :
∀ hz : z ∈ U, (h₁f z hz).order ≠ := by
sorry
theorem MeromorphicOn.decompose
{f : }

View File

@ -348,7 +348,7 @@ theorem makeStronglyMeromorphic_id
· exact m₁ (StronglyMeromorphicAt.meromorphicAt hf) z hz
theorem StronglyMeromorphicAt.decompose
theorem StronglyMeromorphicAt.eliminate
{f : }
{z₀ : }
(h₁f : StronglyMeromorphicAt f z₀)
@ -357,8 +357,6 @@ theorem StronglyMeromorphicAt.decompose
∧ (g z₀ ≠ 0)
∧ (f = (fun z ↦ (z-z₀) ^ (h₁f.meromorphicAt.order.untop h₂f)) * g) := by
let n := - h₁f.meromorphicAt.order.untop h₂f
let g₁ := (fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f)) * f
let g₁₁ := fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f)
have h₁g₁₁ : MeromorphicAt g₁₁ z₀ := by