From 8e5ada9a01cdbb42619d01f6984ddb2ff564b321 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 10 Sep 2024 14:43:28 +0200
Subject: [PATCH] =?UTF-8?q?working=E2=80=A6?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Nevanlinna/analyticAt.lean         | 11 +++++++++++
 Nevanlinna/analyticOn_zeroSet.lean | 21 +++++++--------------
 2 files changed, 18 insertions(+), 14 deletions(-)

diff --git a/Nevanlinna/analyticAt.lean b/Nevanlinna/analyticAt.lean
index c823777..0be7e3a 100644
--- a/Nevanlinna/analyticAt.lean
+++ b/Nevanlinna/analyticAt.lean
@@ -74,3 +74,14 @@ theorem AnalyticAt.order_eq_zero_iff
     · constructor
       · exact hz
       · simp
+
+
+theorem AnalyticAt.supp_order_toNat
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : AnalyticAt ℂ f z₀) :
+  hf.order.toNat ≠ 0 → f z₀ = 0 := by
+
+  contrapose
+  intro h₁f
+  simp [hf.order_eq_zero_iff.2 h₁f]
diff --git a/Nevanlinna/analyticOn_zeroSet.lean b/Nevanlinna/analyticOn_zeroSet.lean
index 5011a37..80d95bf 100644
--- a/Nevanlinna/analyticOn_zeroSet.lean
+++ b/Nevanlinna/analyticOn_zeroSet.lean
@@ -107,16 +107,6 @@ theorem AnalyticOn.support_of_order₁
   rw [not_iff_comm, (hf u u.2).order_eq_zero_iff]
 
 
-theorem AnalyticOn.support_of_order₂
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (h₁U : IsPreconnected U)
-  (h₁f : AnalyticOn ℂ f U)
-  (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  Function.support (ENat.toNat ∘ h₁f.order) = U.restrict f⁻¹' {0} := by
-  sorry
-
-
 theorem AnalyticOn.eliminateZeros
   {f : ℂ → ℂ}
   {U : Set ℂ}
@@ -376,6 +366,7 @@ theorem AnalyticOnCompact.eliminateZeros₁
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
   ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ᶠ a : U, (z - a) ^ (h₁f.order a).toNat) • g z := by
 
+
   let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset
 
   let n : U → ℕ := fun z ↦ (h₁f z z.2).order.toNat
@@ -394,7 +385,6 @@ theorem AnalyticOnCompact.eliminateZeros₁
     intro z
     rw [h₃g z]
 
-
   constructor
   · exact h₁g
   · constructor
@@ -411,14 +401,17 @@ theorem AnalyticOnCompact.eliminateZeros₁
         rw [inter z] at this
         exact right_ne_zero_of_smul this
     · intro z
+
       let φ : U → ℂ := fun a ↦ (z - ↑a) ^ (h₁f.order a).toNat
       have hφ : Function.mulSupport φ ⊆ A := by
         intro x hx
         simp [φ] at hx
         have : (h₁f.order x).toNat ≠ 0 := by
-          sorry
-
-        sorry
+          by_contra C
+          rw [C] at hx
+          simp at hx
+        simp [A]
+        exact AnalyticAt.supp_order_toNat (h₁f x x.2) this
       rw [finprod_eq_prod_of_mulSupport_subset φ hφ]
       rw [inter z]
       rfl