Working…

Nevanlinna/stronglyMeromorphicAt.lean

@@ -84,6 +84,44 @@ theorem AnalyticAt.stronglyMeromorphicAt
     tauto
 
 
+/- Strong meromorphic depends only on germ -/
+theorem stronglyMeromorphicAt_congr
+  {f g : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hfg : f =ᶠ[𝓝 z₀] g) :
+  StronglyMeromorphicAt f z₀ ↔ StronglyMeromorphicAt g z₀ := by
+  unfold StronglyMeromorphicAt
+  constructor
+  · intro h
+    rcases h with h|h
+    · left
+      exact Filter.EventuallyEq.rw h (fun x => Eq (g x)) (id (Filter.EventuallyEq.symm hfg))
+    · obtain ⟨n, h, h₁h, h₂h, h₃h⟩ := h
+      right
+      use n
+      use h
+      constructor
+      · assumption
+      · constructor
+        · assumption
+        · apply Filter.EventuallyEq.trans hfg.symm
+          assumption
+  · intro h
+    rcases h with h|h
+    · left
+      exact Filter.EventuallyEq.rw h (fun x => Eq (f x)) hfg
+    · obtain ⟨n, h, h₁h, h₂h, h₃h⟩ := h
+      right
+      use n
+      use h
+      constructor
+      · assumption
+      · constructor
+        · assumption
+        · apply Filter.EventuallyEq.trans hfg
+          assumption
+
+
 /- Make strongly MeromorphicAt -/
 noncomputable def MeromorphicAt.makeStronglyMeromorphicAt
   {f : ℂ → ℂ}

Nevanlinna/stronglyMeromorphicOn.lean

@@ -45,6 +45,32 @@ theorem AnalyticOn.stronglyMeromorphicOn
   exact h₁f z hz
 
 
+/- Strongly meromorphic functions on compact, preconnected sets are quotients of analytic functions -/
+theorem StronglyMeromorphicOn_finite
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁U : IsCompact U)
+  (h₂U : IsPreconnected U)
+  (h₁f : StronglyMeromorphicOn f U)
+  (h₂f : ∃ z ∈ U, f z ≠ 0) :
+  Set.Finite {z ∈ U | f z = 0} := by
+
+  sorry
+
+
+/- Strongly meromorphic functions on compact, preconnected sets are quotients of analytic functions -/
+theorem StronglyMeromorphicOn_quotient
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁U : IsCompact U)
+  (h₂U : IsPreconnected U)
+  (h₁f : StronglyMeromorphicOn f U)
+  (h₂f : ∃ z ∈ U, f z ≠ 0) :
+  ∃ a b : ℂ → ℂ, (AnalyticOnNhd ℂ a U) ∧ (AnalyticOnNhd ℂ b U) ∧ (∀ z ∈ U, a z ≠ 0 ∨ b z ≠ 0) ∧ f = a / b := by
+
+  sorry
+
+
 /- Make strongly MeromorphicAt -/
 noncomputable def MeromorphicOn.makeStronglyMeromorphicOn
   {f : ℂ → ℂ}
@@ -57,9 +83,48 @@ noncomputable def MeromorphicOn.makeStronglyMeromorphicOn
   · exact f z
 
 
+theorem makeStronglyMeromorphicOn_changeDiscrete
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicOn f U)
+  (hz₀ : z₀ ∈ U) :
+  hf.makeStronglyMeromorphicOn =ᶠ[𝓝[≠] z₀] f := by
+  apply Filter.eventually_iff_exists_mem.2
+  let A := (hf z₀ hz₀).eventually_analyticAt
+  obtain ⟨V, h₁V, h₂V⟩  := Filter.eventually_iff_exists_mem.1 A
+  use V
+  constructor
+  · assumption
+  · intro v hv
+    unfold MeromorphicOn.makeStronglyMeromorphicOn
+    by_cases h₂v : v ∈ U
+    · simp [h₂v]
+      rw [← makeStronglyMeromorphic_id]
+      exact AnalyticAt.stronglyMeromorphicAt (h₂V v hv)
+    · simp [h₂v]
+
+
+theorem makeStronglyMeromorphicOn_changeDiscrete'
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicOn f U)
+  (hz₀ : z₀ ∈ U) :
+  hf.makeStronglyMeromorphicOn =ᶠ[𝓝 z₀] (hf z₀ hz₀).makeStronglyMeromorphicAt := by
+  apply Mnhds
+  let A := makeStronglyMeromorphicOn_changeDiscrete hf hz₀
+  apply Filter.EventuallyEq.trans A
+  exact m₂ (hf z₀ hz₀)
+  unfold MeromorphicOn.makeStronglyMeromorphicOn
+  simp [hz₀]
+
+
 theorem StronglyMeromorphicOn_of_makeStronglyMeromorphicOn
   {f : ℂ → ℂ}
   {U : Set ℂ}
   (hf : MeromorphicOn f U) :
   StronglyMeromorphicOn hf.makeStronglyMeromorphicOn U := by
-  sorry
+  intro z₀ hz₀
+  rw [stronglyMeromorphicAt_congr (makeStronglyMeromorphicOn_changeDiscrete' hf hz₀)]
+  exact StronglyMeromorphicAt_of_makeStronglyMeromorphic (hf z₀ hz₀)