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

working

This commit is contained in:
Stefan Kebekus 2024-11-14 16:18:32 +01:00
parent f22cea20a0
commit fb642a4ed0
2 changed files with 12 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
Nevanlinna/meromorphicOn_decompose.lean
View File

@ -10,6 +10,17 @@ import Nevanlinna.mathlibAddOn
open scoped Interval Topology open scoped Interval Topology
open Real Filter MeasureTheory intervalIntegral 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 theorem MeromorphicOn.decompose
{f : ℂ → ℂ} {f : ℂ → ℂ}

2
Nevanlinna/stronglyMeromorphicAt.lean
View File

@ -348,7 +348,7 @@ theorem makeStronglyMeromorphic_id
· exact m₁ (StronglyMeromorphicAt.meromorphicAt hf) z hz · exact m₁ (StronglyMeromorphicAt.meromorphicAt hf) z hz
theorem StronglyMeromorphicAt.decompose theorem StronglyMeromorphicAt.eliminate
{f : ℂ → ℂ} {f : ℂ → ℂ}
{z₀ : ℂ} {z₀ : ℂ}
(h₁f : StronglyMeromorphicAt f z₀) (h₁f : StronglyMeromorphicAt f z₀)