working

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
@@ -125,6 +170,35 @@ theorem stronglyMeromorphicAt_congr
           assumption
 
 
+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 : ℂ → ℂ}
   {z₀ : ℂ}

Nevanlinna/stronglyMeromorphicOn_eliminate.lean

@@ -14,10 +14,10 @@ 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)
@@ -146,14 +146,42 @@ theorem MeromorphicOn.decompose₁
 theorem MeromorphicOn.decompose₂
   {f : ℂ → ℂ}
   {U : Set ℂ}
-  {P : Finset ℂ}
-  (hP : P.toSet ⊆ U)
-  (h₁f : MeromorphicOn f U)
-  (h₂f : ∀ hp : p ∈ P, StronglyMeromorphicAt f p)
-  (h₃f : ∀ hp : p ∈ P, (h₂f hp).meromorphicAt.order ≠ ⊤) :
-  ∃ g : ℂ → ℂ, (MeromorphicOn g U)
-    ∧ (∀ p ∈ P, AnalyticAt ℂ g p)
-    ∧ (∀ p ∈ P, g p ≠ 0)
-    ∧ (f = g * ∏ p ∈ P, fun z ↦ (z - p) ^ (h₁f.divisor p)) := by
+  {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
 
-  sorry
+  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₅g₀ : StronglyMeromorphicAt g₀ u := by
+
+    sorry
+  have h₆g₀ : (h₁g₀ u u.2).order ≠ ⊤ := by
+    sorry
+
+  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
+      · constructor
+        · sorry
+        · sorry