Update analyticOn_zeroSet.lean

Nevanlinna/analyticOn_zeroSet.lean

@@ -1,21 +1,25 @@
 import Mathlib.Analysis.Analytic.Constructions
 import Mathlib.Analysis.Analytic.IsolatedZeros
 import Mathlib.Analysis.Complex.Basic
+import Nevanlinna.analyticAt
+
+
+noncomputable def AnalyticOn.order
+  {f : ℂ → ℂ} {U : Set ℂ} (hf : AnalyticOn ℂ f U) : U → ℕ∞ := fun u ↦ (hf u u.2).order
 
 
 theorem AnalyticOn.order_eq_nat_iff
   {f : ℂ → ℂ}
   {U : Set ℂ}
-  {z₀ : ℂ}
+  {z₀ : U}
   (hf : AnalyticOn ℂ f U)
-  (hz₀ : z₀ ∈ U)
   (n : ℕ) :
-  (hf z₀ hz₀).order = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by
+  hf.order z₀ = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by
 
   constructor
   -- Direction →
   intro hn
-  obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ hz₀) n).1 hn
+  obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ z₀.2) n).1 hn
 
   -- Define a candidate function; this is (f z) / (z - z₀) ^ n with the
   -- removable singularity removed
@@ -44,7 +48,7 @@ theorem AnalyticOn.order_eq_nat_iff
   have g_near_z₁ {z₁ : ℂ} : z₁ ≠ z₀ → ∀ᶠ (z : ℂ) in nhds z₁, g z = f z / (z - z₀) ^ n := by
     intro hz₁
     rw [eventually_nhds_iff]
-    use {z₀}ᶜ
+    use {z₀.1}ᶜ
     constructor
     · intro y hy
       simp at hy
@@ -87,59 +91,10 @@ theorem AnalyticOn.order_eq_nat_iff
   -- direction ←
   intro h
   obtain ⟨g, h₁g, h₂g, h₃g⟩ := h
+  dsimp [AnalyticOn.order]
   rw [AnalyticAt.order_eq_nat_iff]
   use g
-  exact ⟨h₁g z₀ hz₀, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩
-
-
-theorem AnalyticAt.order_mul
-  {f₁ f₂ : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf₁ : AnalyticAt ℂ f₁ z₀)
-  (hf₂ : AnalyticAt ℂ f₂ z₀) :
-  (AnalyticAt.mul hf₁ hf₂).order = hf₁.order + hf₂.order := by
-  by_cases h₂f₁ : hf₁.order = ⊤
-  · simp [h₂f₁]
-    rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff]
-    rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at h₂f₁
-    obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₁
-    use t
-    constructor
-    · intro y hy
-      rw [h₁t y hy]
-      ring
-    · exact ⟨h₂t, h₃t⟩
-  · by_cases h₂f₂ : hf₂.order = ⊤
-    · simp [h₂f₂]
-      rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff]
-      rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at h₂f₂
-      obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₂
-      use t
-      constructor
-      · intro y hy
-        rw [h₁t y hy]
-        ring
-      · exact ⟨h₂t, h₃t⟩
-    · obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticAt.order_eq_nat_iff hf₁ ↑hf₁.order.toNat).1 (eq_comm.1 (ENat.coe_toNat h₂f₁))
-      obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (AnalyticAt.order_eq_nat_iff hf₂ ↑hf₂.order.toNat).1 (eq_comm.1 (ENat.coe_toNat h₂f₂))
-      rw [← ENat.coe_toNat h₂f₁, ← ENat.coe_toNat h₂f₂, ← ENat.coe_add]
-      rw [AnalyticAt.order_eq_nat_iff (AnalyticAt.mul hf₁ hf₂) ↑(hf₁.order.toNat + hf₂.order.toNat)]
-      use g₁ * g₂
-      constructor
-      · exact AnalyticAt.mul h₁g₁ h₁g₂
-      · constructor
-        · simp; tauto
-        · obtain ⟨t₁, h₁t₁, h₂t₁, h₃t₁⟩ := eventually_nhds_iff.1 h₃g₁
-          obtain ⟨t₂, h₁t₂, h₂t₂, h₃t₂⟩ := eventually_nhds_iff.1 h₃g₂
-          rw [eventually_nhds_iff]
-          use t₁ ∩ t₂
-          constructor
-          · intro y hy
-            rw [h₁t₁ y hy.1, h₁t₂ y hy.2]
-            simp; ring
-          · constructor
-            · exact IsOpen.inter h₂t₁ h₂t₂
-            · exact Set.mem_inter h₃t₁ h₃t₂
+  exact ⟨h₁g z₀ z₀.2, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩
 
 
 theorem AnalyticOn.eliminateZeros
@@ -148,7 +103,7 @@ theorem AnalyticOn.eliminateZeros
   {A : Finset U}
   (hf : AnalyticOn ℂ f U)
   (n : ℂ → ℕ) :
-  (∀ 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 := by
+  (∀ 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)
 
@@ -208,8 +163,7 @@ theorem AnalyticOn.eliminateZeros
     rw [h₂φ]
     simp
 
-
-  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ b₀.2 (n b₀)).1 this
+  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ (n b₀)).1 this
 
   use g₁
   constructor
@@ -259,14 +213,14 @@ theorem discreteZeros
   (hU : IsPreconnected U)
   (h₁f : AnalyticOn ℂ f U)
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  DiscreteTopology ↑(U ∩ f⁻¹' {0}) := by
+  DiscreteTopology ((U.restrict f)⁻¹' {0}) := by
 
   simp_rw [← singletons_open_iff_discrete]
   simp_rw [Metric.isOpen_singleton_iff]
 
   intro z
 
-  let A := XX hU h₁f h₂f z.2.1
+  let A := XX hU h₁f h₂f z.1.2
   rw [eq_comm] at A
   rw [AnalyticAt.order_eq_nat_iff] at A
   obtain ⟨g, h₁g, h₂g, h₃g⟩ := A
@@ -311,9 +265,9 @@ theorem discreteZeros
     _ < min ε₁ ε₂ := by assumption
     _ ≤ ε₁ := by exact min_le_left ε₁ ε₂
 
-
   have F := h₂ε₂ y.1 h₂y
-  rw [y.2.2] at F
+  have : f y = 0 := by exact y.2
+  rw [this] at F
   simp at F
 
   have : g y.1 ≠ 0 := by
@@ -331,19 +285,19 @@ theorem finiteZeros
   (h₂U : IsCompact U)
   (h₁f : AnalyticOn ℂ f U)
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  Set.Finite ↑(U ∩ f⁻¹' {0}) := by
+  Set.Finite (U.restrict f⁻¹' {0}) := by
 
-  have hinter : IsCompact ↑(U ∩ f⁻¹' {0}) := by
-    apply IsCompact.of_isClosed_subset h₂U
-    apply h₁f.continuousOn.preimage_isClosed_of_isClosed
-    exact IsCompact.isClosed h₂U
+  have closedness : IsClosed (U.restrict f⁻¹' {0}) := by
+    apply IsClosed.preimage
+    apply continuousOn_iff_continuous_restrict.1
+    exact h₁f.continuousOn
     exact isClosed_singleton
-    exact Set.inter_subset_left
 
-  apply hinter.finite
-  apply DiscreteTopology.of_subset (s := ↑(U ∩ f⁻¹' {0}))
+  have : CompactSpace U := by
+    exact isCompact_iff_compactSpace.mp h₂U
+
+  apply (IsClosed.isCompact closedness).finite
   exact discreteZeros h₁U h₁f h₂f
-  rfl
 
 
 theorem AnalyticOnCompact.eliminateZeros
@@ -355,15 +309,7 @@ theorem AnalyticOnCompact.eliminateZeros
   (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
 
-  let ι : U → ℂ := Subtype.val
-
-  let A₁ := ι⁻¹' (U ∩ f⁻¹' {0})
-
-  have : A₁.Finite := by
-    apply Set.Finite.preimage
-    exact Set.injOn_subtype_val
-    exact finiteZeros h₁U h₂U h₁f h₂f
-  let A := this.toFinset
+  let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset
 
   let n : ℂ → ℕ := by
     intro z
@@ -400,14 +346,10 @@ theorem AnalyticOnCompact.eliminateZeros
       · exact h₂g ⟨z, h₁z⟩ h₂z
       · have : f z ≠ 0 := by
           by_contra C
-          have : ⟨z, h₁z⟩ ∈ ↑A₁ := by
-            dsimp [A₁, ι]
-            simp
-            exact C
           have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by
             dsimp [A]
             simp
-            exact this
+            exact C
           tauto
         rw [inter z] at this
         exact right_ne_zero_of_smul this