Update stronglyMeromorphicAt.lean

Nevanlinna/mathlibAddOn.lean

@@ -37,21 +37,6 @@ theorem ContDiff.const_smul' {f : E → F} (c : R) (hf : ContDiff 𝕜 n f) :
   exact ContDiff.const_smul c hf
 
 
--- Mathlib.Analysis.Analytic.Meromorphic
-
-theorem meromorphicAt_congr
-  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
-  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-  {f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜}
-  (h : f =ᶠ[nhdsWithin x {x}ᶜ] g) : MeromorphicAt f x ↔ MeromorphicAt g x :=
-  ⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩
-
-theorem meromorphicAt_congr'
-  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
-  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-  {f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜}
-  (h : f =ᶠ[nhds x] g) : MeromorphicAt f x ↔ MeromorphicAt g x :=
-  meromorphicAt_congr (Filter.EventuallyEq.filter_mono h nhdsWithin_le_nhds)
 
 open Topology Filter
 

Nevanlinna/meromorphicAt.lean

@@ -7,6 +7,22 @@ open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
 
 
+theorem meromorphicAt_congr
+  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
+  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+  {f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜}
+  (h : f =ᶠ[nhdsWithin x {x}ᶜ] g) : MeromorphicAt f x ↔ MeromorphicAt g x :=
+  ⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩
+
+
+theorem meromorphicAt_congr'
+  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
+  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+  {f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜}
+  (h : f =ᶠ[nhds x] g) : MeromorphicAt f x ↔ MeromorphicAt g x :=
+  meromorphicAt_congr (Filter.EventuallyEq.filter_mono h nhdsWithin_le_nhds)
+
+
 theorem MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero
   {f : ℂ → ℂ}
   {z₀ : ℂ}
@@ -53,6 +69,7 @@ theorem MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero
       · exact h₂N
       · exact h₃N
 
+
 theorem MeromorphicAt.order_congr
   {f₁ f₂ : ℂ → ℂ}
   {z₀ : ℂ}
@@ -73,3 +90,58 @@ theorem MeromorphicAt.order_congr
     · constructor
       · assumption
       · exact EventuallyEq.rw h₃g (fun x => Eq (f₂ x)) (_root_.id (EventuallyEq.symm h))
+
+
+theorem MeromorphicAt.order_mul
+  {f₁ f₂ : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf₁ : MeromorphicAt f₁ z₀)
+  (hf₂ : MeromorphicAt f₂ z₀) :
+  (hf₁.mul hf₂).order = hf₁.order + hf₂.order := by
+  by_cases h₂f₁ : hf₁.order = ⊤
+  · simp [h₂f₁]
+    rw [hf₁.order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] at h₂f₁
+    rw [(hf₁.mul hf₂).order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff]
+    obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₁
+    use t
+    constructor
+    · intro y h₁y h₂y
+      simp; left
+      rw [h₁t y h₁y h₂y]
+    · exact ⟨h₂t, h₃t⟩
+  · by_cases h₂f₂ : hf₂.order = ⊤
+    · simp [h₂f₂]
+      rw [hf₂.order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] at h₂f₂
+      rw [(hf₁.mul hf₂).order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff]
+      obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₂
+      use t
+      constructor
+      · intro y h₁y h₂y
+        simp; right
+        rw [h₁t y h₁y h₂y]
+      · exact ⟨h₂t, h₃t⟩
+    · have h₃f₁ := Eq.symm (WithTop.coe_untop hf₁.order h₂f₁)
+      have h₃f₂ := Eq.symm (WithTop.coe_untop hf₂.order h₂f₂)
+      obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (hf₁.order_eq_int_iff (hf₁.order.untop h₂f₁)).1 h₃f₁
+      obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (hf₂.order_eq_int_iff (hf₂.order.untop h₂f₂)).1 h₃f₂
+      rw [h₃f₁, h₃f₂, ← WithTop.coe_add]
+      rw [MeromorphicAt.order_eq_int_iff]
+      use g₁ * g₂
+      constructor
+      · exact AnalyticAt.mul h₁g₁ h₁g₂
+      · constructor
+        · simp; tauto
+        · obtain ⟨t₁, h₁t₁, h₂t₁, h₃t₁⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₃g₁)
+          obtain ⟨t₂, h₁t₂, h₂t₂, h₃t₂⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₃g₂)
+          rw [eventually_nhdsWithin_iff, eventually_nhds_iff]
+          use t₁ ∩ t₂
+          constructor
+          · intro y h₁y h₂y
+            simp
+            rw [h₁t₁ y h₁y.1 h₂y, h₁t₂ y h₁y.2 h₂y]
+            simp
+            rw [zpow_add' (by left; exact sub_ne_zero_of_ne h₂y)]
+            group
+          · constructor
+            · exact IsOpen.inter h₂t₁ h₂t₂
+            · exact Set.mem_inter h₃t₁ h₃t₂

Nevanlinna/stronglyMeromorphicAt.lean

@@ -1,4 +1,5 @@
 import Mathlib.Analysis.Analytic.Meromorphic
+import Mathlib.Algebra.Order.AddGroupWithTop
 import Nevanlinna.analyticAt
 import Nevanlinna.mathlibAddOn
 import Nevanlinna.meromorphicAt
@@ -199,6 +200,8 @@ theorem StronglyMeromorphicAt.localIdentity
 
 
 
+
+
 /- Make strongly MeromorphicAt -/
 noncomputable def MeromorphicAt.makeStronglyMeromorphicAt
   {f : ℂ → ℂ}
@@ -346,3 +349,56 @@ theorem makeStronglyMeromorphic_id
         tauto
 
   · exact m₁ (StronglyMeromorphicAt.meromorphicAt hf) z hz
+
+
+theorem StronglyMeromorphicAt.decompose
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (h₁f : StronglyMeromorphicAt f z₀)
+  (h₂f : h₁f.meromorphicAt.order ≠ ⊤) :
+  ∃ g : ℂ → ℂ, (AnalyticAt ℂ g z₀)
+    ∧ (g z₀ ≠ 0)
+    ∧ (f = (fun z ↦ (z-z₀) ^ (h₁f.meromorphicAt.order.untop h₂f)) * g) := by
+
+  let n := - h₁f.meromorphicAt.order.untop h₂f
+
+  let g₁ := (fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f)) * f
+  let g₁₁ := fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f)
+  have h₁g₁₁ : MeromorphicAt g₁₁ z₀ := by
+    apply MeromorphicAt.zpow
+    apply AnalyticAt.meromorphicAt
+    apply AnalyticAt.sub
+    apply analyticAt_id
+    exact analyticAt_const
+  have h₂g₁₁ : h₁g₁₁.order = - h₁f.meromorphicAt.order.untop h₂f := by
+    rw [← WithTop.LinearOrderedAddCommGroup.coe_neg]
+    rw [h₁g₁₁.order_eq_int_iff]
+    use 1
+    constructor
+    · exact analyticAt_const
+    · constructor
+      · simp
+      · apply eventually_nhdsWithin_of_forall
+        simp [g₁₁]
+  have h₁g₁ : MeromorphicAt g₁ z₀ := h₁g₁₁.mul h₁f.meromorphicAt
+  have h₂g₁ : h₁g₁.order = 0 := by
+    rw [h₁g₁₁.order_mul h₁f.meromorphicAt]
+    rw [h₂g₁₁]
+    simp
+    rw [add_comm]
+    rw [LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top h₂f]
+  let g := h₁g₁.makeStronglyMeromorphicAt
+  use g
+  have h₁g : StronglyMeromorphicAt g z₀ := by
+    exact StronglyMeromorphicAt_of_makeStronglyMeromorphic h₁g₁
+  have h₂g : h₁g.meromorphicAt.order = 0 := by
+    rw [← h₁g₁.order_congr (m₂ h₁g₁)]
+    exact h₂g₁
+  constructor
+  · apply analytic
+    · rw [h₂g]
+    · exact h₁g
+  · constructor
+    · exact (order_eq_zero_iff h₁g).mp h₂g
+    ·
+      sorry