Update analyticOn_zeroSet.lean

Nevanlinna/analyticOn_zeroSet.lean

@@ -102,7 +102,7 @@ theorem AnalyticOn.eliminateZeros
   {U : Set ℂ}
   {A : Finset U}
   (hf : AnalyticOn ℂ f U)
-  (n : ℂ → ℕ) :
+  (n : U → ℕ) :
   (∀ a ∈ A, hf.order a = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z := by
 
   apply Finset.induction (α := U) (p := fun A ↦ (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z)
@@ -122,7 +122,7 @@ theorem AnalyticOn.eliminateZeros
 
     rw [← hBinsert b₀ (Finset.mem_insert_self b₀ B)]
 
-    let φ := fun z ↦ (∏ a ∈ B, (z - a.1) ^ n a.1)
+    let φ := fun z ↦ (∏ a ∈ B, (z - a.1) ^ n a)
 
     have : f = fun z ↦ φ z * g₀ z := by
       funext z
@@ -307,7 +307,54 @@ theorem AnalyticOnCompact.eliminateZeros
   (h₂U : IsCompact U)
   (h₁f : AnalyticOn ℂ f U)
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  ∃ (g : ℂ → ℂ) (A : Finset U), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (h₁f a a.2).order.toNat) • g z := by
+  ∃ (g : ℂ → ℂ) (A : Finset U), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (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
+
+  have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
+    intro a _
+    dsimp [n, AnalyticOn.order]
+    rw [eq_comm]
+    apply XX h₁U
+    exact h₂f
+
+
+  obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
+  use g
+  use A
+
+  have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by
+    intro z
+    rw [h₃g z]
+
+  constructor
+  · exact h₁g
+  · constructor
+    · intro z h₁z
+      by_cases h₂z : ⟨z, h₁z⟩  ∈ ↑A.toSet
+      · exact h₂g ⟨z, h₁z⟩ h₂z
+      · have : f z ≠ 0 := by
+          by_contra C
+          have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by
+            dsimp [A]
+            simp
+            exact C
+          tauto
+        rw [inter z] at this
+        exact right_ne_zero_of_smul this
+    · exact inter
+
+
+theorem AnalyticOnCompact.eliminateZeros₁
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁U : IsPreconnected U)
+  (h₂U : IsCompact U)
+  (h₁f : AnalyticOn ℂ f U)
+  (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
 
@@ -327,9 +374,8 @@ theorem AnalyticOnCompact.eliminateZeros
 
   obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
   use g
-  use A
 
-  have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by
+  have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f.order a).toNat) • g z := by
     intro z
     rw [h₃g z]
     congr
@@ -338,6 +384,7 @@ theorem AnalyticOnCompact.eliminateZeros
     dsimp [n]
     simp [a.2]
 
+
   constructor
   · exact h₁g
   · constructor
@@ -353,4 +400,5 @@ theorem AnalyticOnCompact.eliminateZeros
           tauto
         rw [inter z] at this
         exact right_ne_zero_of_smul this
-    · exact inter
+    ·
+      exact inter