Working!

Nevanlinna/analyticAt.lean

@@ -308,3 +308,37 @@ theorem AnalyticAt.zpow
       intro x
       rw [zpow_neg]
     exact AnalyticAt.inv (zpow_nonneg h₁f (by linarith)) (zpow_ne_zero (-n) h₂f)
+
+
+/- A function is analytic at a point iff it is analytic after multiplication
+   with a non-vanishing analytic function
+-/
+theorem analyticAt_of_mul_analytic
+  {f g : ℂ → ℂ}
+  {z₀ : ℂ}
+  (h₁g : AnalyticAt ℂ g z₀)
+  (h₂g : g z₀ ≠ 0) :
+  AnalyticAt ℂ f z₀ ↔ AnalyticAt ℂ (f * g) z₀ := by
+  constructor
+  · exact fun a => AnalyticAt.mul₁ a h₁g
+  · intro hprod
+
+    let g' := fun z ↦ (g z)⁻¹
+    have h₁g' := h₁g.inv h₂g
+    have h₂g' : g' z₀ ≠ 0 := by
+      exact inv_ne_zero h₂g
+
+    have : f =ᶠ[𝓝 z₀] f * g * fun x => (g x)⁻¹ := by
+      unfold Filter.EventuallyEq
+      apply Filter.eventually_iff_exists_mem.mpr
+      use g⁻¹' {0}ᶜ
+      constructor
+      · apply ContinuousAt.preimage_mem_nhds
+        exact AnalyticAt.continuousAt h₁g
+        exact compl_singleton_mem_nhds_iff.mpr h₂g
+      · intro y hy
+        simp at hy
+        simp [hy]
+    rw [analyticAt_congr this]
+    apply hprod.mul
+    exact h₁g'

Nevanlinna/stronglyMeromorphicAt.lean

@@ -15,6 +15,51 @@ 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))
 
 
+lemma stronglyMeromorphicAt_of_mul_analytic'
+  {f g : ℂ → ℂ}
+  {z₀ : ℂ}
+  (h₁g : AnalyticAt ℂ g z₀)
+  (h₂g : g z₀ ≠ 0) :
+  StronglyMeromorphicAt f z₀ → StronglyMeromorphicAt (f * g) z₀ := by
+
+  intro hf
+  --unfold StronglyMeromorphicAt at hf
+  rcases hf with h₁f|h₁f
+  · left
+    rw [eventually_nhds_iff] at h₁f
+    obtain ⟨t, ht⟩ := h₁f
+    rw [eventually_nhds_iff]
+    use t
+    constructor
+    · intro y hy
+      simp
+      left
+      exact ht.1 y hy
+    · exact ht.2
+  · right
+    obtain ⟨n, g_f, h₁g_f, h₂g_f, h₃g_f⟩ := h₁f
+    use n
+    use g * g_f
+    constructor
+    · apply AnalyticAt.mul
+      exact h₁g
+      exact h₁g_f
+    · constructor
+      · simp
+        exact ⟨h₂g, h₂g_f⟩
+      · rw [eventually_nhds_iff] at h₃g_f
+        obtain ⟨t, ht⟩ := h₃g_f
+        rw [eventually_nhds_iff]
+        use t
+        constructor
+        · intro y hy
+          simp
+          rw [ht.1]
+          simp
+          ring
+          exact hy
+        · exact ht.2
+
 
 /- Strongly MeromorphicAt is Meromorphic -/
 theorem StronglyMeromorphicAt.meromorphicAt
@@ -124,6 +169,37 @@ theorem stronglyMeromorphicAt_congr
         · apply Filter.EventuallyEq.trans hfg
           assumption
 
+/- A function is strongly meromorphic at a point iff it is strongly meromorphic
+   after multiplication with a non-vanishing analytic function
+-/
+theorem stronglyMeromorphicAt_of_mul_analytic
+  {f g : ℂ → ℂ}
+  {z₀ : ℂ}
+  (h₁g : AnalyticAt ℂ g z₀)
+  (h₂g : g z₀ ≠ 0) :
+  StronglyMeromorphicAt f z₀ ↔ StronglyMeromorphicAt (f * g) z₀ := by
+  constructor
+  · apply stronglyMeromorphicAt_of_mul_analytic' h₁g h₂g
+  · intro hprod
+    let g' := fun z ↦ (g z)⁻¹
+    have h₁g' := h₁g.inv h₂g
+    have h₂g' : g' z₀ ≠ 0 := by
+      exact inv_ne_zero h₂g
+
+    let B := stronglyMeromorphicAt_of_mul_analytic' h₁g' h₂g' (f := f * g) hprod
+    have : f =ᶠ[𝓝 z₀] f * g * fun x => (g x)⁻¹ := by
+      unfold Filter.EventuallyEq
+      apply Filter.eventually_iff_exists_mem.mpr
+      use g⁻¹' {0}ᶜ
+      constructor
+      · apply ContinuousAt.preimage_mem_nhds
+        exact AnalyticAt.continuousAt h₁g
+        exact compl_singleton_mem_nhds_iff.mpr h₂g
+      · intro y hy
+        simp at hy
+        simp [hy]
+    rwa [stronglyMeromorphicAt_congr this]
+
 
 theorem StronglyMeromorphicAt.order_eq_zero_iff
   {f : ℂ → ℂ}

Nevanlinna/stronglyMeromorphicOn_eliminate.lean

@@ -10,22 +10,14 @@ import Nevanlinna.mathlibAddOn
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
 
-lemma untop_eq_untop'
-  {n : WithTop ℤ}
-  (hn : n ≠ ⊤) :
-  n.untop' 0 = n.untop hn := by
-  rw [WithTop.untop'_eq_iff]
-  simp
-
-
 theorem MeromorphicOn.decompose₁
   {f : ℂ → ℂ}
   {U : Set ℂ}
   {z₀ : ℂ}
-  (hz₀ : z₀ ∈ U)
   (h₁f : MeromorphicOn f U)
   (h₂f : StronglyMeromorphicAt f z₀)
-  (h₃f : h₂f.meromorphicAt.order ≠ ⊤) :
+  (h₃f : h₂f.meromorphicAt.order ≠ ⊤)
+  (hz₀ : z₀ ∈ U) :
   ∃ g : ℂ → ℂ, (MeromorphicOn g U)
     ∧ (AnalyticAt ℂ g z₀)
     ∧ (g z₀ ≠ 0)
@@ -149,3 +141,152 @@ theorem MeromorphicOn.decompose₁
           simp
           apply zpow_ne_zero
           rwa [sub_ne_zero]
+
+
+theorem MeromorphicOn.decompose₂
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  {P : Finset U}
+  (hf : StronglyMeromorphicOn f U) :
+  (∀ p ∈ P, (hf p p.2).meromorphicAt.order ≠ ⊤) →
+    ∃ g : ℂ → ℂ, (MeromorphicOn g U)
+    ∧ (∀ p : P, AnalyticAt ℂ g p)
+    ∧ (∀ p : P, g p ≠ 0)
+    ∧ (f = g * ∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by
+
+  apply Finset.induction (p := fun (P : Finset U) ↦
+    (∀ p ∈ P, (hf p p.2).meromorphicAt.order ≠ ⊤) →
+    ∃ g : ℂ → ℂ, (MeromorphicOn g U)
+    ∧ (∀ p : P, AnalyticAt ℂ g p)
+    ∧ (∀ p : P, g p ≠ 0)
+    ∧ (f = g * ∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)))
+
+  -- case empty
+  simp
+  exact hf.meromorphicOn
+
+  -- case insert
+  intro u P hu iHyp
+  intro hOrder
+  obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀, h₄g₀⟩ := iHyp (fun p hp ↦ hOrder p (Finset.mem_insert_of_mem hp))
+
+  have h₀ : AnalyticAt ℂ (∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) u := by
+    have : (∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) = (fun z => ∏ p : P, (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by
+      funext w
+      simp
+    rw [this]
+    apply Finset.analyticAt_prod
+    intro p hp
+    apply AnalyticAt.zpow
+    apply AnalyticAt.sub
+    apply analyticAt_id
+    apply analyticAt_const
+    by_contra hCon
+    rw [sub_eq_zero] at hCon
+    have : p.1 = u := by
+      exact SetCoe.ext (_root_.id (Eq.symm hCon))
+    rw [← this] at hu
+    simp [hp] at hu
+
+  have h₁ : (∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) u ≠ 0 := by
+    simp only [Finset.prod_apply]
+    rw [Finset.prod_ne_zero_iff]
+    intro p hp
+    apply zpow_ne_zero
+    by_contra hCon
+    rw [sub_eq_zero] at hCon
+    have : p.1 = u := by
+      exact SetCoe.ext (_root_.id (Eq.symm hCon))
+    rw [← this] at hu
+    simp [hp] at hu
+
+  have h₅g₀ : StronglyMeromorphicAt g₀ u := by
+    rw [stronglyMeromorphicAt_of_mul_analytic h₀ h₁]
+    rw [← h₄g₀]
+    exact hf u u.2
+
+  have h₆g₀ : (h₁g₀ u u.2).order ≠ ⊤ := by
+    by_contra hCon
+    let A := (h₁g₀ u u.2).order_mul h₀.meromorphicAt
+    simp_rw [← h₄g₀, hCon] at A
+    simp at A
+    let B := hOrder u (Finset.mem_insert_self u P)
+    tauto
+
+  obtain ⟨g, h₁g, h₂g, h₃g, h₄g⟩ := h₁g₀.decompose₁ h₅g₀ h₆g₀ u.2
+  use g
+  · constructor
+    · exact h₁g
+    · constructor
+      · intro ⟨v₁, v₂⟩
+        simp
+        simp at v₂
+        rcases v₂ with hv|hv
+        · rwa [hv]
+        · let A := h₂g₀ ⟨v₁, hv⟩
+          rw [h₄g] at A
+          rw [← analyticAt_of_mul_analytic] at A
+          simp at A
+          exact A
+          --
+          simp
+          apply AnalyticAt.zpow
+          apply AnalyticAt.sub
+          apply analyticAt_id
+          apply analyticAt_const
+          by_contra hCon
+          rw [sub_eq_zero] at hCon
+
+          have : v₁ = u := by
+            exact SetCoe.ext hCon
+          rw [this] at hv
+          tauto
+          --
+          apply zpow_ne_zero
+          simp
+          by_contra hCon
+          rw [sub_eq_zero] at hCon
+          have : v₁ = u := by
+            exact SetCoe.ext hCon
+          rw [this] at hv
+          tauto
+
+      · constructor
+        · intro ⟨v₁, v₂⟩
+          simp
+          simp at v₂
+          rcases v₂ with hv|hv
+          · rwa [hv]
+          · by_contra hCon
+            let A := h₃g₀ ⟨v₁,hv⟩
+            rw [h₄g] at A
+            simp at A
+            tauto
+        · conv =>
+            left
+            rw [h₄g₀, h₄g]
+          simp
+          rw [mul_assoc]
+          congr
+          rw [Finset.prod_insert]
+          simp
+          congr
+          have : (hf u u.2).meromorphicAt.order = (h₁g₀ u u.2).order := by
+            have h₅g₀ : f =ᶠ[𝓝 u.1] (g₀ * ∏ p : P, fun z => (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by
+              exact Eq.eventuallyEq h₄g₀
+            have h₆g₀ : f =ᶠ[𝓝[≠] u.1] (g₀ * ∏ p : P, fun z => (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by
+              exact eventuallyEq_nhdsWithin_of_eqOn fun ⦃x⦄ a => congrFun h₄g₀ x
+            rw [(hf u u.2).meromorphicAt.order_congr h₆g₀]
+            let C := (h₁g₀ u u.2).order_mul h₀.meromorphicAt
+            rw [C]
+            let D := h₀.order_eq_zero_iff.2 h₁
+            let E := h₀.meromorphicAt_order
+            rw [E, D]
+            simp
+          have : hf.meromorphicOn.divisor u = h₁g₀.divisor u := by
+            unfold MeromorphicOn.divisor
+            simp
+            rw [this]
+          rw [this]
+          --
+          simpa