Nevanlinna/analyticOn_zeroSet.lean

@@ -100,44 +100,89 @@ theorem AnalyticOn.order_eq_nat_iff'
   {U : Set ℂ}
   {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
+  (n : A → ℕ) :
+  ∀ a : A, (hf a (Subtype.coe_prop a.val)).order = n a → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a, g a ≠ 0) ∧ ∀ z, f z = (∏ 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)
+  apply Finset.induction
 
-  -- case empty
-  simp
-  use f
-  simp
-  exact hf
+  let a : A := by sorry
+  let b : ℂ := by sorry
+  let u : U := by sorry
 
-  -- case insert
-  intro b₀ B hb iHyp
-  intro hBinsert
-  obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀⟩ := iHyp (fun a ha ↦ hBinsert a (Finset.mem_insert_of_mem ha))
+  let X := n a
+  have : a = (3 : ℂ) := by sorry
+  have : b ∈ ↑A := by sorry
+  have : ↑a ∈ U := by exact Subtype.coe_prop a.val
 
-  have : (h₁g₀ b₀ b₀.2).order = n b₀ := by sorry
-  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ b₀.2 (n b₀)).1 this
+  let Y := ∀ a : A, (hf a (Subtype.coe_prop a.val)).order = n a
 
-  use g₁
+  --∀ a : A, (hf (ha a)).order = ↑(n a) →
+
+  intro hn
+  obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ hz₀) n).1 hn
+
+  -- Define a candidate function
+  let g : ℂ → ℂ := fun z ↦ if z = z₀ then gloc z₀ else (f z) / (z - z₀) ^ n
+
+  -- Describe g near z₀
+  have g_near_z₀ : ∀ᶠ (z : ℂ) in nhds z₀, g z = gloc z := by
+    rw [eventually_nhds_iff]
+    obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 h₃gloc
+    use t
     constructor
-  · exact h₁g₁
+    · intro y h₁y
+      by_cases h₂y : y = z₀
+      · dsimp [g]; simp [h₂y]
+      · dsimp [g]; simp [h₂y]
+        rw [div_eq_iff_mul_eq, eq_comm, mul_comm]
+        exact h₁t y h₁y
+        norm_num
+        rw [sub_eq_zero]
+        tauto
     · constructor
-    · intro a h₁a
-      by_cases h₂a : a = b₀
-      · rwa [h₂a]
-      · let A' := Finset.mem_of_mem_insert_of_ne h₁a h₂a
-        let B' := h₃g₁ a
-        let C' := h₂g₀ a A'
-        rw [B'] at C'
-        exact right_ne_zero_of_smul C'
-    · intro z
-      let A' := h₃g₀ z
-      rw [h₃g₁ z] at A'
-      rw [A']
-      rw [← smul_assoc]
-      congr
+      · assumption
+      · assumption
+
+  -- Describe g near points z₁ different from z₀
+  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₀}ᶜ
+    constructor
+    · intro y hy
+      simp at hy
+      simp [g, hy]
+    · exact ⟨isOpen_compl_singleton, hz₁⟩
+
+  -- Use g and show that it has all required properties
+  use g
+  constructor
+  · -- AnalyticOn ℂ g U
+    intro z h₁z
+    by_cases h₂z : z = z₀
+    · rw [h₂z]
+      apply AnalyticAt.congr h₁gloc
+      exact Filter.EventuallyEq.symm g_near_z₀
+    · simp_rw [eq_comm] at g_near_z₁
+      apply AnalyticAt.congr _ (g_near_z₁ h₂z)
+      apply AnalyticAt.div
+      exact hf z h₁z
+      apply AnalyticAt.pow
+      apply AnalyticAt.sub
+      apply analyticAt_id
+      apply analyticAt_const
       simp
-      rw [Finset.prod_insert]
-      ring
-      exact hb
+      rw [sub_eq_zero]
+      tauto
+  · constructor
+    · simp [g]; tauto
+    · intro z
+      by_cases h₂z : z = z₀
+      · rw [h₂z, g_near_z₀.self_of_nhds]
+        exact h₃gloc.self_of_nhds
+      · rw [(g_near_z₁ h₂z).self_of_nhds]
+        simp [h₂z]
+        rw [div_eq_mul_inv, mul_comm, mul_assoc, inv_mul_cancel]
+        simp; norm_num
+        rw [sub_eq_zero]
+        tauto