From ccdbb319f7fcae02415f1bb6695034a2085bf522 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 24 Oct 2024 14:05:16 +0200
Subject: [PATCH] Create stronglyMeromorphicOn.lean

---
 Nevanlinna/stronglyMeromorphicOn.lean | 175 ++++++++++++++++++++++++++
 1 file changed, 175 insertions(+)
 create mode 100644 Nevanlinna/stronglyMeromorphicOn.lean

diff --git a/Nevanlinna/stronglyMeromorphicOn.lean b/Nevanlinna/stronglyMeromorphicOn.lean
new file mode 100644
index 0000000..fee12b5
--- /dev/null
+++ b/Nevanlinna/stronglyMeromorphicOn.lean
@@ -0,0 +1,175 @@
+import Nevanlinna.stronglyMeromorphicAt
+
+
+open Topology
+
+
+/- Strongly MeromorphicOn -/
+def StronglyMeromorphicOn
+  (f : ℂ → ℂ)
+  (U : Set ℂ) :=
+  ∀ z ∈ U, StronglyMeromorphicAt f z
+
+
+/- Strongly MeromorphicAt is Meromorphic -/
+theorem StronglyMeromorphicOn.meromorphicOn
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hf : StronglyMeromorphicOn f U) :
+  MeromorphicOn f U := by
+  intro z hz
+  exact StronglyMeromorphicAt.meromorphicAt (hf z hz)
+
+
+/- Strongly MeromorphicOn of non-negative order is analytic -/
+theorem StronglyMeromorphicOn.analytic
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁f : StronglyMeromorphicOn f U)
+  (h₂f : ∀ x, (hx : x ∈ U) → 0 ≤ (h₁f x hx).meromorphicAt.order):
+  ∀ z ∈ U, AnalyticAt ℂ f z := by
+  intro z hz
+  apply StronglyMeromorphicAt.analytic
+  exact h₂f z hz
+  exact h₁f z hz
+
+
+/- Analytic functions are strongly meromorphic -/
+theorem AnalyticOn.stronglyMeromorphicOn
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁f : AnalyticOn ℂ f U) :
+  StronglyMeromorphicOn f U := by
+  intro z hz
+  apply AnalyticAt.stronglyMeromorphicAt
+  let A := h₁f z hz
+  exact h₁f z hz
+
+
+/- Make strongly MeromorphicAt -/
+noncomputable def MeromorphicAt.makeStronglyMeromorphicAt
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicAt f z₀) :
+  ℂ → ℂ := by
+  intro z
+  by_cases z = z₀
+  · by_cases h₁f : hf.order = (0 : ℤ)
+    · rw [hf.order_eq_int_iff] at h₁f
+      exact (Classical.choose h₁f) z₀
+    · exact 0
+  · exact f z
+
+
+lemma m₁
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicAt f z₀) :
+  ∀ z ≠ z₀, f z = hf.makeStronglyMeromorphicAt z := by
+  intro z hz
+  unfold MeromorphicAt.makeStronglyMeromorphicAt
+  simp [hz]
+
+
+lemma m₂
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicAt f z₀) :
+  f =ᶠ[𝓝[≠] z₀] hf.makeStronglyMeromorphicAt := by
+  apply eventually_nhdsWithin_of_forall
+  exact fun x a => m₁ hf x a
+
+
+lemma Mnhds
+  {f g : ℂ → ℂ}
+  {z₀ : ℂ}
+  (h₁ : f =ᶠ[𝓝[≠] z₀] g)
+  (h₂ : f z₀ = g z₀) :
+  f =ᶠ[𝓝 z₀] g := by
+  apply eventually_nhds_iff.2
+  obtain ⟨t, h₁t, h₂t⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₁)
+  use t
+  constructor
+  · intro y hy
+    by_cases h₂y : y ∈ ({z₀}ᶜ : Set ℂ)
+    · exact h₁t y hy h₂y
+    · simp at h₂y
+      rwa [h₂y]
+  · exact h₂t
+
+
+theorem localIdentity
+  {f g : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : AnalyticAt ℂ f z₀)
+  (hg : AnalyticAt ℂ g z₀) :
+  f =ᶠ[𝓝[≠] z₀] g → f =ᶠ[𝓝 z₀] g := by
+  intro h
+  let Δ := f - g
+  have : AnalyticAt ℂ Δ z₀ := AnalyticAt.sub hf hg
+  have t₁ : Δ =ᶠ[𝓝[≠] z₀] 0 := by
+    exact Filter.eventuallyEq_iff_sub.mp h
+
+  have : Δ =ᶠ[𝓝 z₀] 0 := by
+    rcases (AnalyticAt.eventually_eq_zero_or_eventually_ne_zero this) with h | h
+    · exact h
+    · have := Filter.EventuallyEq.eventually t₁
+      let A := Filter.eventually_and.2 ⟨this, h⟩
+      let _ := Filter.Eventually.exists A
+      tauto
+  exact Filter.eventuallyEq_iff_sub.mpr this
+
+
+theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicAt f z₀) :
+  StronglyMeromorphicAt hf.makeStronglyMeromorphicAt z₀ := by
+
+  by_cases h₂f : hf.order = ⊤
+  · have : hf.makeStronglyMeromorphicAt =ᶠ[𝓝 z₀] 0 := by
+      apply Mnhds
+      · apply Filter.EventuallyEq.trans (Filter.EventuallyEq.symm (m₂ hf))
+        exact (MeromorphicAt.order_eq_top_iff hf).1 h₂f
+      · unfold MeromorphicAt.makeStronglyMeromorphicAt
+        simp [h₂f]
+
+    apply AnalyticAt.stronglyMeromorphicAt
+    rw [analyticAt_congr this]
+    apply analyticAt_const
+  · let n := hf.order.untop h₂f
+    have : hf.order = n := by
+      exact Eq.symm (WithTop.coe_untop hf.order h₂f)
+    rw [hf.order_eq_int_iff] at this
+    obtain ⟨g, h₁g, h₂g, h₃g⟩ := this
+    right
+    use n
+    use g
+    constructor
+    · assumption
+    · constructor
+      · assumption
+      · apply Mnhds
+        · apply Filter.EventuallyEq.trans (Filter.EventuallyEq.symm (m₂ hf))
+          exact h₃g
+        · unfold MeromorphicAt.makeStronglyMeromorphicAt
+          simp
+          by_cases h₃f : hf.order = (0 : ℤ)
+          · let h₄f := (hf.order_eq_int_iff 0).1 h₃f
+            simp [h₃f]
+            obtain ⟨h₁G, h₂G, h₃G⟩  := Classical.choose_spec h₄f
+            simp at h₃G
+            have hn : n = 0 := Eq.symm ((fun {α} {a} {b} h => (WithTop.eq_untop_iff h).mpr) h₂f (id (Eq.symm h₃f)))
+            rw [hn]
+            rw [hn] at h₃g; simp at h₃g
+            simp
+            have : g =ᶠ[𝓝 z₀] (Classical.choose h₄f) := by
+              apply localIdentity h₁g h₁G
+              exact Filter.EventuallyEq.trans (Filter.EventuallyEq.symm h₃g) h₃G
+            rw [Filter.EventuallyEq.eq_of_nhds this]
+          · have : hf.order ≠ 0 := h₃f
+            simp [this]
+            left
+            apply zero_zpow n
+            dsimp [n]
+            rwa [WithTop.untop_eq_iff h₂f]