nevanlinna/Nevanlinna/meromorphicOn.lean

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 : Set U := Subtype.val ⁻¹' t'
  use t
  constructor
  · intro w hw
    simp
    rw [MeromorphicAt.order_eq_top_iff]

    sorry
  · constructor
    · exact isOpen_induced h₂t'
    · exact h₃t'

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⟩