56 lines
1.3 KiB
Plaintext
56 lines
1.3 KiB
Plaintext
import Mathlib.Analysis.Analytic.Meromorphic
|
||
import Nevanlinna.analyticAt
|
||
import Nevanlinna.divisor
|
||
import Nevanlinna.meromorphicAt
|
||
import Nevanlinna.meromorphicOn_divisor
|
||
import Nevanlinna.stronglyMeromorphicOn
|
||
import Nevanlinna.mathlibAddOn
|
||
|
||
open scoped Interval Topology
|
||
open Real Filter MeasureTheory intervalIntegral
|
||
|
||
theorem MeromorphicOn.open_of_order_eq_top
|
||
{f : ℂ → ℂ}
|
||
{U : Set ℂ}
|
||
(h₁f : MeromorphicOn f U) :
|
||
IsOpen { u : U | (h₁f u.1 u.2).order = ⊤ } := by
|
||
|
||
apply isOpen_iff_forall_mem_open.mpr
|
||
intro z hz
|
||
simp at hz
|
||
rw [MeromorphicAt.order_eq_top_iff] at hz
|
||
rw [eventually_nhdsWithin_iff] at hz
|
||
rw [eventually_nhds_iff] at hz
|
||
obtain ⟨t', h₁t', h₂t', h₃t'⟩ := hz
|
||
let t :=
|
||
have : t ⊆ { u : U | (h₁f u.1 u.2).order = ⊤} := by
|
||
sorry
|
||
|
||
|
||
|
||
rw [← eventually_eventually_nhds] at hz
|
||
|
||
|
||
sorry
|
||
|
||
|
||
theorem MeromorphicOn.order_ne_top
|
||
{f : ℂ → ℂ}
|
||
{U : Set ℂ}
|
||
(h₁U : IsConnected U)
|
||
(h₁f : MeromorphicOn f U) :
|
||
(∃ z₀ : U, (h₁f z₀.1 z₀.2).order = ⊤) ↔ (∀ z : U, (h₁f z.1 z.2).order = ⊤) := by
|
||
|
||
constructor
|
||
· intro h
|
||
obtain ⟨h₁z₀, h₂z₀⟩ := h
|
||
intro hz
|
||
|
||
|
||
sorry
|
||
|
||
· intro h
|
||
obtain ⟨w, hw⟩ := h₁U.nonempty
|
||
use ⟨w, hw⟩
|
||
exact h ⟨w, hw⟩
|