Working…

Nevanlinna/meromorphicOn_divisor.lean

@@ -100,3 +100,23 @@ theorem MeromorphicOn.divisor_def₂
   rw [WithTop.untop'_eq_iff]
   left
   exact Eq.symm (WithTop.coe_untop (hf z hz).order h₂f)
+
+
+theorem MeromorphicOn.divisor_mul
+  {f₁ f₂ : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁f₁ : MeromorphicOn f₁ U)
+  (h₂f₁ : ∀ z, (hz : z ∈ U) → (h₁f₁ z hz).order ≠ ⊤)
+  (h₁f₂ : MeromorphicOn f₂ U)
+  (h₂f₂ : ∀ z, (hz : z ∈ U) → (h₁f₂ z hz).order ≠ ⊤) :
+  (h₁f₁.mul h₁f₂).divisor.toFun = h₁f₁.divisor.toFun + h₁f₂.divisor.toFun := by
+  funext z
+
+  by_cases hz : z ∈ U
+  · simp [hz]
+    rw [MeromorphicOn.divisor_def₂ h₁f₁ hz (h₂f₁ z hz)]
+    rw [MeromorphicOn.divisor_def₂ h₁f₂ hz (h₂f₂ z hz)]
+    let A := MeromorphicAt.order_mul (h₁f₁ z hz) (h₁f₂ z hz)
+    sorry
+  · unfold MeromorphicOn.divisor
+    simp [hz]

Nevanlinna/stronglyMeromorphicOn_eliminate.lean

@@ -1,4 +1,5 @@
 import Mathlib.Analysis.Analytic.Meromorphic
+import Mathlib.Data.Set.Finite
 import Nevanlinna.analyticAt
 import Nevanlinna.divisor
 import Nevanlinna.meromorphicAt
@@ -325,16 +326,35 @@ theorem MeromorphicOn.decompose₃
       rw [A] at this
       tauto
 
-  have h₄f : Finite (Function.support h₁f.meromorphicOn.divisor) := by
+  have h₄f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := by
     exact h₁f.meromorphicOn.divisor.finiteSupport h₁U
 
   let P' : Set U := Subtype.val ⁻¹' Function.support h₁f.meromorphicOn.divisor
-  have : Finite P' := by
+  let P := (h₄f.preimage Set.injOn_subtype_val : Set.Finite P').toFinset
-    unfold P'
+  have hP : ∀ p ∈ P, (h₁f p p.2).meromorphicAt.order ≠ ⊤ := by
-    refine Finite.of_injective ?f ?H
+    intro p hp
+    apply h₃f
+
+  obtain ⟨g, h₁g, h₂g, h₃g, h₄g⟩ := MeromorphicOn.decompose₂ h₁f (P := P) hP
+  let h := ∏ p ∈ P, fun z => (z - p.1) ^ h₁f.meromorphicOn.divisor p.1
+  have h₁h : MeromorphicOn h U := by
+    sorry
+  have h₂h : StronglyMeromorphicOn h U := by
+    sorry
+  have h₃h : h₁h.divisor = h₁f.meromorphicOn.divisor := by
+    sorry
+
+
+  use g
+  constructor
+  · exact h₁g
+  · constructor
+    · sorry
+    · constructor
+      · sorry
+      · conv =>
+          left
+          rw [h₄g]
+        congr
         simp
-    apply Finite.of_injective
-    sorry
-
-
         sorry