Nevanlinna/mathlibAddOn.lean

@@ -37,6 +37,21 @@ 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,22 +7,6 @@ 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₀ : ℂ}
@@ -69,7 +53,6 @@ theorem MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero
       · exact h₂N
       · exact h₃N
 
-
 theorem MeromorphicAt.order_congr
   {f₁ f₂ : ℂ → ℂ}
   {z₀ : ℂ}
@@ -90,58 +73,3 @@ 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,5 +1,4 @@
 import Mathlib.Analysis.Analytic.Meromorphic
-import Mathlib.Algebra.Order.AddGroupWithTop
 import Nevanlinna.analyticAt
 import Nevanlinna.mathlibAddOn
 import Nevanlinna.meromorphicAt
@@ -200,8 +199,6 @@ theorem StronglyMeromorphicAt.localIdentity
 
 
 
-
-
 /- Make strongly MeromorphicAt -/
 noncomputable def MeromorphicAt.makeStronglyMeromorphicAt
   {f : ℂ → ℂ}
@@ -349,56 +346,3 @@ 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