nevanlinna/Nevanlinna/meromorphicOn.lean

76 lines
1.9 KiB
Plaintext
Raw Normal View History

2024-11-14 16:53:35 +01:00
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
2024-11-15 12:16:41 +01:00
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
2024-11-18 18:44:42 +01:00
have h₁z := hz
2024-11-15 12:16:41 +01:00
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
2024-11-16 13:24:50 +01:00
let t : Set U := Subtype.val ⁻¹' t'
use t
constructor
· intro w hw
simp
2024-11-18 18:44:42 +01:00
by_cases h₁w : w = z
· rwa [h₁w]
· --
rw [MeromorphicAt.order_eq_top_iff]
rw [eventually_nhdsWithin_iff]
rw [eventually_nhds_iff]
use t' \ {z.1}
constructor
· intro y h₁y h₂y
apply h₁t'
exact Set.mem_of_mem_diff h₁y
exact Set.mem_of_mem_inter_right h₁y
· constructor
· apply IsOpen.sdiff h₂t'
exact isClosed_singleton
· rw [Set.mem_diff]
constructor
· exact hw
· simp
exact Subtype.coe_ne_coe.mpr h₁w
2024-11-17 16:56:27 +01:00
2024-11-16 13:24:50 +01:00
· constructor
· exact isOpen_induced h₂t'
· exact h₃t'
2024-11-15 12:16:41 +01:00
2024-11-14 16:53:35 +01:00
theorem MeromorphicOn.order_ne_top
{f : }
{U : Set }
(h₁U : IsConnected U)
(h₁f : MeromorphicOn f U) :
2024-11-15 09:01:55 +01:00
(∃ z₀ : U, (h₁f z₀.1 z₀.2).order = ) ↔ (∀ z : U, (h₁f z.1 z.2).order = ) := by
2024-11-14 16:53:35 +01:00
constructor
· intro h
obtain ⟨h₁z₀, h₂z₀⟩ := h
intro hz
2024-11-15 09:01:55 +01:00
2024-11-14 16:53:35 +01:00
sorry
· intro h
obtain ⟨w, hw⟩ := h₁U.nonempty
use ⟨w, hw⟩
exact h ⟨w, hw⟩