From a910bd6988b1d1f379c62a541a99f2f7ba275759 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 19 Aug 2024 14:08:00 +0200
Subject: [PATCH] Update holomorphic_zero.lean

---
 Nevanlinna/holomorphic_zero.lean | 106 ++++++++++++++++++++-----------
 1 file changed, 70 insertions(+), 36 deletions(-)

diff --git a/Nevanlinna/holomorphic_zero.lean b/Nevanlinna/holomorphic_zero.lean
index 508d57d..59d2ef3 100644
--- a/Nevanlinna/holomorphic_zero.lean
+++ b/Nevanlinna/holomorphic_zero.lean
@@ -36,6 +36,17 @@ theorem zeroDivisor_eq_ord_AtZeroDivisorSupport
   simp [analyticAtZeroDivisorSupport h]
 
 
+theorem zeroDivisor_eq_ord_AtZeroDivisorSupport'
+  {f : ℂ → ℂ}
+  {z : ℂ}
+  (h : z ∈ Function.support (zeroDivisor f)) :
+  zeroDivisor f z = (analyticAtZeroDivisorSupport h).order := by
+
+  unfold zeroDivisor
+  simp [analyticAtZeroDivisorSupport h]
+  sorry
+
+
 lemma toNatEqSelf_iff {n : ℕ∞} : n.toNat = n ↔ ∃ m : ℕ, m = n := by
   constructor
   · intro H₁
@@ -338,52 +349,75 @@ theorem AnalyticOn.order_eq_nat_iff
       tauto
 
 
-theorem eliminatingZeros
+noncomputable def zeroDivisorDegree
   {f : ℂ → ℂ}
   {U : Set ℂ}
-  (h₁U : IsPreconnected U)
+  (h₁U : IsPreconnected U) -- not needed!
   (h₂U : IsCompact U)
   (h₁f : AnalyticOn ℂ f U)
-  (h₂f : ∃ z ∈ U, f z ≠ 0) :
+  (h₂f : ∃ z ∈ U, f z ≠ 0) : -- not needed!
+  ℕ := (zeroDivisor_finiteOnCompact h₁U h₁f h₂f h₂U).toFinset.card
+
+
+lemma zeroDivisorDegreeZero
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁U : IsPreconnected U) -- not needed!
+  (h₂U : IsCompact U)
+  (h₁f : AnalyticOn ℂ f U)
+  (h₂f : ∃ z ∈ U, f z ≠ 0) : -- not needed!
+  0 = zeroDivisorDegree h₁U h₂U h₁f h₂f ↔ U ∩ (zeroDivisor f).support = ∅ := by
+  sorry
+
+
+lemma eliminatingZeros₀
+  {U : Set ℂ}
+  (h₁U : IsPreconnected U)
+  (h₂U : IsCompact U) :
+  ∀ n : ℕ, ∀ f : ℂ → ℂ, (h₁f : AnalyticOn ℂ f U) → (h₂f : ∃ z ∈ U, f z ≠ 0) →
+  (n = zeroDivisorDegree h₁U h₂U h₁f h₂f) →
   ∃ F : ℂ → ℂ, (AnalyticOn ℂ F U) ∧ (f = F * ∏ᶠ a ∈ (U ∩ (zeroDivisor f).support), fun z ↦ (z - a) ^ (zeroDivisor f a)) := by
 
-  have hs := zeroDivisor_finiteOnCompact h₁U h₁f h₂f h₂U
-  rw [finprod_mem_eq_finite_toFinset_prod _ hs]
+  intro n
+  induction' n with n ih
+  -- case zero
+  intro f h₁f h₂f h₃f
+  use f
+  rw [zeroDivisorDegreeZero] at h₃f
+  rw [h₃f]
+  simpa
 
-  let A := hs.card_eq
+  -- case succ
+  intro f h₁f h₂f h₃f
+
+  let Supp := (zeroDivisor_finiteOnCompact h₁U h₁f h₂f h₂U).toFinset
+
+  have : Supp.Nonempty := by
+    rw [← Finset.one_le_card]
+    calc 1
+    _ ≤ n + 1 := by exact Nat.le_add_left 1 n
+    _ = zeroDivisorDegree h₁U h₂U h₁f h₂f := by exact h₃f
+    _ = Supp.card := by rfl
+  obtain ⟨z₀, hz₀⟩ := this
+  dsimp [Supp] at hz₀
+  simp only [Set.Finite.mem_toFinset, Set.mem_inter_iff] at hz₀
 
 
 
-  let F : ℂ → ℂ := by
-    intro z
-    if hz : z ∈ U ∩ (zeroDivisor f).support then
-      exact (Classical.choose (zeroDivisor_support_iff.1 hz.2).2.2) z
-    else
-      exact (f z) / ∏ i ∈ hs.toFinset, (z - i) ^ zeroDivisor f i
 
+  let A := AnalyticOn.order_eq_nat_iff h₁f hz₀.1 (zeroDivisor f z₀)
+  let B := zeroDivisor_eq_ord_AtZeroDivisorSupport hz₀.2
+  let B := zeroDivisor_eq_ord_AtZeroDivisorSupport' hz₀.2
+  rw [eq_comm] at B
+  let C := A B
+  obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀⟩ := C
+
+  have h₄g₀ : ∃ z ∈ U, g₀ z ≠ 0 := by sorry
+  have h₅g₀ : n = zeroDivisorDegree h₁U h₂U h₁g₀ h₄g₀ := by sorry
+
+  obtain ⟨F, h₁F, h₂F⟩ := ih g₀ h₁g₀ h₄g₀ h₅g₀
   use F
   constructor
-  · intro z h₁z
-    by_cases h₂z : z ∈ (zeroDivisor f).support
-    · -- case: z ∈ Function.support (zeroDivisor f)
-      have : z ∈ U ∩ (zeroDivisor f).support := by exact Set.mem_inter h₁z h₂z
-
-
-      sorry
-  · sorry
-
-  have : MeromorphicOn F U := by
-    apply MeromorphicOn.div
-    exact AnalyticOn.meromorphicOn h₁f
-    apply AnalyticOn.meromorphicOn
-    apply Finset.analyticOn_prod
-    intro n hn
-    apply AnalyticOn.pow
-    apply AnalyticOn.sub
-    exact analyticOn_id ℂ
-    exact analyticOn_const
-
-  --use F
-
-
-  sorry
+  · assumption
+  ·
+    sorry