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

@@ -169,7 +169,9 @@ 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₀ : ℂ}

Nevanlinna/stronglyMeromorphicOn_eliminate.lean

@@ -170,12 +170,7 @@ theorem MeromorphicOn.decompose₂
   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₅g₀ : StronglyMeromorphicAt g₀ u := by
-
-    rw [stronglyMeromorphicAt_of_mul_analytic (g := ∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) (z₀ := u) (f := g₀)]
-    rw [← h₄g₀]
-    exact hf u u.2
-    --
+  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
@@ -186,14 +181,14 @@ theorem MeromorphicOn.decompose₂
     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
@@ -205,16 +200,93 @@ theorem MeromorphicOn.decompose₂
     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
-    sorry
+    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
-      · sorry
+      · 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
-        · sorry
-        · sorry
+        · 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