Update analyticOn_zeroSet.lean

Nevanlinna/analyticOn_zeroSet.lean

@@ -346,7 +346,6 @@ theorem finiteZeros
   rfl
 
 
-
 theorem AnalyticOnCompact.eliminateZeros
   {f : ℂ → ℂ}
   {U : Set ℂ}
@@ -354,95 +353,60 @@ theorem AnalyticOnCompact.eliminateZeros
   (h₂U : IsCompact U)
   (h₁f : AnalyticOn ℂ f U)
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ U, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z := by
+  ∃ (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
 
+  let ι : U → ℂ := Subtype.val
 
-  let A := U ∩ f ⁻¹' {0}
+  let A₁ := ι⁻¹' (U ∩ f⁻¹' {0})
 
-  by sorry -- (finiteZeros h₁U h₂U h₁f h₂f).toFinset
+  have t₁ : (U ∩ f⁻¹' {0}).Finite := by
-  let B := AnalyticOn.eliminateZeros h₁f
+    sorry
 
+  have : A₁.Finite := by
+    apply Set.Finite.preimage
+    exact Set.injOn_subtype_val
+    exact t₁
+  let A := this.toFinset
 
-  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)
+  let n : ℂ → ℕ := by
+    intro z
+    by_cases hz : z ∈ U
+    · exact (h₁f z hz).order.toNat
+    · exact 0
 
-  -- case empty
+  have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
-  simp
+    sorry
-  use f
-  simp
-  exact hf
 
-  -- case insert
+  obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
-  intro b₀ B hb iHyp
+  use g
-  intro hBinsert
+  use A
-  obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀⟩ := iHyp (fun a ha ↦ hBinsert a (Finset.mem_insert_of_mem ha))
 
-  have : (h₁g₀ b₀ b₀.2).order = n b₀ := by
+  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]
+    congr
+    funext a
+    congr
+    dsimp [n]
+    simp [a.2]
 
-    rw [← hBinsert b₀ (Finset.mem_insert_self b₀ B)]
-
-    let φ := fun z ↦ (∏ a ∈ B, (z - a.1) ^ n a.1)
-
-    have : f = fun z ↦ φ z * g₀ z := by
-      funext z
-      rw [h₃g₀ z]
-      rfl
-    simp_rw [this]
-
-    have h₁φ : AnalyticAt ℂ φ b₀ := by
-      dsimp [φ]
-      apply Finset.analyticAt_prod
-      intro b _
-      apply AnalyticAt.pow
-      apply AnalyticAt.sub
-      apply analyticAt_id ℂ
-      exact analyticAt_const
-
-    have h₂φ : h₁φ.order = (0 : ℕ) := by
-      rw [AnalyticAt.order_eq_nat_iff h₁φ 0]
-      use φ
-      constructor
-      · assumption
-      · constructor
-        · dsimp [φ]
-          push_neg
-          rw [Finset.prod_ne_zero_iff]
-          intro a ha
-          simp
-          have : ¬ (b₀.1 - a.1 = 0) := by
-            by_contra C
-            rw [sub_eq_zero] at C
-            rw [SetCoe.ext C] at hb
-            tauto
-          tauto
-        · simp
-
-    rw [AnalyticAt.order_mul h₁φ (h₁g₀ b₀ b₀.2)]
-
-    rw [h₂φ]
-    simp
-
-
-  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ b₀.2 (n b₀)).1 this
-
-  use g₁
   constructor
-  · exact h₁g₁
+  · exact h₁g
   · constructor
-    · intro a h₁a
+    · intro z h₁z
-      by_cases h₂a : a = b₀
+      by_cases h₂z : ⟨z, h₁z⟩  ∈ ↑A.toSet
-      · rwa [h₂a]
+      · exact h₂g ⟨z, h₁z⟩ h₂z
-      · let A' := Finset.mem_of_mem_insert_of_ne h₁a h₂a
+      · have : f z ≠ 0 := by
-        let B' := h₃g₁ a
+          by_contra C
-        let C' := h₂g₀ a A'
+          have : ⟨z, h₁z⟩ ∈ ↑A₁ := by
-        rw [B'] at C'
+            dsimp [A₁, ι]
-        exact right_ne_zero_of_smul C'
+            simp
-    · intro z
+            exact C
-      let A' := h₃g₀ z
+          have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by
-      rw [h₃g₁ z] at A'
+            dsimp [A]
-      rw [A']
+            simp
-      rw [← smul_assoc]
+            exact this
-      congr
+          tauto
-      simp
+        rw [inter z] at this
-      rw [Finset.prod_insert]
+        exact right_ne_zero_of_smul this
-      ring
+    · exact inter
-      exact hb