Create analyticOn_zeroSet.lean

Nevanlinna/analyticOn_zeroSet.lean

@@ -0,0 +1,188 @@
+import Init.Classical
+import Mathlib.Analysis.Analytic.Meromorphic
+import Mathlib.Topology.ContinuousOn
+import Mathlib.Analysis.Analytic.IsolatedZeros
+import Nevanlinna.holomorphic
+
+
+
+theorem AnalyticOn.order_eq_nat_iff
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  {z₀ : ℂ}
+  (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
+
+  constructor
+  -- Direction →
+  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; this is (f z) / (z - z₀) ^ n with the
+  -- removable singularity removed
+  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
+    · 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
+      · assumption
+      · assumption
+
+  -- Describe g near points z₁ that are 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 [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
+
+  -- direction ←
+  intro h
+  obtain ⟨g, h₁g, h₂g, h₃g⟩ := h
+  rw [AnalyticAt.order_eq_nat_iff]
+  use g
+  exact ⟨h₁g z₀ hz₀, ⟨h₂g, Filter.eventually_of_forall h₃g⟩⟩
+
+
+theorem AnalyticOn.order_eq_nat_iff'
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  {A : Finset U}
+  (hf : AnalyticOn ℂ f U)
+  (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
+
+  let a : A := by sorry
+  let b : ℂ := by sorry
+  let u : U := by sorry
+
+  let X := n a
+  have : a = (3 : ℂ) := by sorry
+  have : b ∈ ↑A := by sorry
+  have : ↑a ∈ U := by exact Subtype.coe_prop a.val
+
+  let Y := ∀ a : A, (hf a (Subtype.coe_prop a.val)).order = n a
+
+  --∀ 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
+    · 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
+      · 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 [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