Working…

Nevanlinna/analyticAt.lean

@@ -2,6 +2,8 @@ import Mathlib.Analysis.Analytic.IsolatedZeros
 import Mathlib.Analysis.Complex.Basic
 import Mathlib.Analysis.Analytic.Linear
 
+open Topology
+
 
 theorem AnalyticAt.order_neq_top_iff
   {f : ℂ → ℂ}
@@ -236,3 +238,25 @@ theorem AnalyticAt.order_comp_CLE
     rw [this]
 
     simp
+
+
+theorem AnalyticAt.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

Nevanlinna/meromorphicAt.lean

@@ -52,3 +52,24 @@ theorem MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero
     · constructor
       · exact h₂N
       · exact h₃N
+
+theorem MeromorphicAt.order_congr
+  {f₁ f₂ : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf₁ : MeromorphicAt f₁ z₀)
+  (h : f₁ =ᶠ[𝓝[≠] z₀] f₂):
+  hf₁.order = (hf₁.congr h).order := by
+  by_cases hord : hf₁.order = ⊤
+  · rw [hord, eq_comm]
+    rw [hf₁.order_eq_top_iff] at hord
+    rw [(hf₁.congr h).order_eq_top_iff]
+    exact EventuallyEq.rw hord (fun x => Eq (f₂ x)) (_root_.id (EventuallyEq.symm h))
+  · obtain ⟨n, hn : hf₁.order = n⟩ := Option.ne_none_iff_exists'.mp hord
+    obtain ⟨g, h₁g, h₂g, h₃g⟩ := (hf₁.order_eq_int_iff n).1 hn
+    rw [hn, eq_comm, (hf₁.congr h).order_eq_int_iff]
+    use g
+    constructor
+    · assumption
+    · constructor
+      · assumption
+      · exact EventuallyEq.rw h₃g (fun x => Eq (f₂ x)) (_root_.id (EventuallyEq.symm h))

Nevanlinna/meromorphicOn_decompose.lean

@@ -24,6 +24,7 @@ lemma WithTopCoe
     rw [this]
     rfl
 
+
 theorem MeromorphicOn.decompose
   {f : ℂ → ℂ}
   {U : Set ℂ}
@@ -70,5 +71,11 @@ theorem MeromorphicOn.decompose
       rw [hn]
       exact A
     · intro z hz
+      have t₀ : ∀ᶠ x in 𝓝[≠] z, AnalyticAt ℂ f x := by
+        sorry
+      have t₂ : ∀ᶠ x in 𝓝[≠] z, h₁f.divisor z = 0 := by
+        sorry
+      have t₁ : ∀ᶠ x in 𝓝[≠] z, AnalyticAt ℂ (fun z => ∏ᶠ (p : ℂ), (z - p) ^ h₁f.divisor p * g z) x := by
+        sorry
 
       sorry

Nevanlinna/stronglyMeromorphicAt.lean

@@ -1,6 +1,7 @@
 import Mathlib.Analysis.Analytic.Meromorphic
 import Nevanlinna.analyticAt
 import Nevanlinna.mathlibAddOn
+import Nevanlinna.meromorphicAt
 
 
 open Topology
@@ -13,6 +14,7 @@ def StronglyMeromorphicAt
   (∀ᶠ (z : ℂ) in nhds z₀, f z = 0) ∨ (∃ (n : ℤ), ∃ g : ℂ → ℂ, (AnalyticAt ℂ g z₀) ∧ (g z₀ ≠ 0) ∧ (∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ n • g z))
 
 
+
 /- Strongly MeromorphicAt is Meromorphic -/
 theorem StronglyMeromorphicAt.meromorphicAt
   {f : ℂ → ℂ}
@@ -122,6 +124,42 @@ theorem stronglyMeromorphicAt_congr
           assumption
 
 
+theorem StronglyMeromorphicAt.order_eq_zero_iff
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : StronglyMeromorphicAt f z₀) :
+  hf.meromorphicAt.order = 0 ↔ f z₀ ≠ 0 := by
+  sorry
+
+theorem StronglyMeromorphicAt.localIdentity
+  {f g : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : StronglyMeromorphicAt f z₀)
+  (hg : StronglyMeromorphicAt g z₀) :
+  f =ᶠ[𝓝[≠] z₀] g → f =ᶠ[𝓝 z₀] g := by
+
+  intro h
+
+  have t₀ : hf.meromorphicAt.order = hg.meromorphicAt.order := by
+    exact hf.meromorphicAt.order_congr h
+
+  by_cases cs : hf.meromorphicAt.order = 0
+  · rw [cs] at t₀
+    have h₁f := hf.analytic (le_of_eq (id (Eq.symm cs)))
+    have h₁g := hg.analytic (le_of_eq t₀)
+    exact h₁f.localIdentity h₁g h
+  · apply Mnhds h
+    let A := cs
+    rw [hf.order_eq_zero_iff] at A
+    simp at A
+    let B := cs
+    rw [t₀] at B
+    rw [hg.order_eq_zero_iff] at B
+    simp at B
+    rw [A, B]
+
+
+
 /- Make strongly MeromorphicAt -/
 noncomputable def MeromorphicAt.makeStronglyMeromorphicAt
   {f : ℂ → ℂ}
@@ -155,46 +193,6 @@ lemma m₂
   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 : ℂ → ℂ}
@@ -240,7 +238,7 @@ theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
             rw [hn] at h₃g; simp at h₃g
             simp
             have : g =ᶠ[𝓝 z₀] (Classical.choose h₄f) := by
-              apply localIdentity h₁g h₁G
+              apply h₁g.localIdentity 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
@@ -292,7 +290,7 @@ theorem makeStronglyMeromorphic_id
         let A := (h₀f.meromorphicAt.order_eq_int_iff 0).1 t₀
         have : g =ᶠ[𝓝 z₀] (Classical.choose A) := by
           obtain ⟨h₀, h₁, h₂⟩  := Classical.choose_spec A
-          apply localIdentity h₁g h₀
+          apply h₁g.localIdentity h₀
           rw [hn] at h₃g
           simp at h₃g
           simp at h₂