Nevanlinna/analyticAt.lean

@@ -50,27 +50,3 @@ theorem AnalyticAt.order_mul
           · constructor
             · exact IsOpen.inter h₂t₁ h₂t₂
             · exact Set.mem_inter h₃t₁ h₃t₂
-
-
-theorem AnalyticAt.order_eq_zero_iff
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : AnalyticAt ℂ f z₀) :
-  hf.order = 0 ↔ f z₀ ≠ 0 := by
-
-  have : (0 : ENat) = (0 : Nat) := by rfl
-  rw [this, AnalyticAt.order_eq_nat_iff hf 0]
-
-  constructor
-  · intro hz
-    obtain ⟨g, _, h₂g, h₃g⟩ := hz
-    simp at h₃g
-    rw [Filter.Eventually.self_of_nhds h₃g]
-    tauto
-  · intro hz
-    use f
-    constructor
-    · exact hf
-    · constructor
-      · exact hz
-      · simp

Nevanlinna/analyticOn_zeroSet.lean

@@ -97,32 +97,12 @@ theorem AnalyticOn.order_eq_nat_iff
   exact ⟨h₁g z₀ z₀.2, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩
 
 
-theorem AnalyticOn.support_of_order₁
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : AnalyticOn ℂ f U) :
-  Function.support hf.order = U.restrict f⁻¹' {0} := by
-  ext u
-  simp [AnalyticOn.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 ℂ}
   {A : Finset U}
   (hf : AnalyticOn ℂ f U)
-  (n : U → ℕ) :
+  (n : ℂ → ℕ) :
   (∀ 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)
@@ -142,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)
+    let φ := fun z ↦ (∏ a ∈ B, (z - a.1) ^ n a.1)
 
     have : f = fun z ↦ φ z * g₀ z := by
       funext z
@@ -327,20 +307,24 @@ 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.order a).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 a a.2).order.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
+  let n : ℂ → ℕ := by
+    intro z
+    by_cases hz : z ∈ U
+    · exact (h₁f z hz).order.toNat
+    · exact 0
 
   have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
     intro a _
-    dsimp [n, AnalyticOn.order]
+    dsimp [n]
+    simp
     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
@@ -348,6 +332,11 @@ theorem AnalyticOnCompact.eliminateZeros
   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]
 
   constructor
   · exact h₁g
@@ -365,60 +354,3 @@ theorem AnalyticOnCompact.eliminateZeros
         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
-
-  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
-
-  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
-    · 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
-      rw [finprod_eq_prod_of_mulSupport_subset φ hφ]
-      rw [inter z]
-      rfl