Working…

Nevanlinna/analyticAt.lean

@@ -282,6 +282,17 @@ theorem analyticAt_finprod
     exact analyticAt_const
 
 
+lemma AnalyticAt.zpow_nonneg
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  {n : ℤ}
+  (hf : AnalyticAt ℂ f z₀)
+  (hn : 0 ≤ n) :
+  AnalyticAt ℂ (fun x ↦ (f x) ^ n) z₀ := by
+  simp_rw [(Eq.symm (Int.toNat_of_nonneg hn) : n = OfNat.ofNat n.toNat), zpow_ofNat]
+  apply AnalyticAt.pow hf
+
+
 theorem AnalyticAt.zpow
   {f : ℂ → ℂ}
   {z₀ : ℂ}
@@ -289,5 +300,11 @@ theorem AnalyticAt.zpow
   (h₁f : AnalyticAt ℂ f z₀)
   (h₂f : f z₀ ≠ 0) :
   AnalyticAt ℂ (fun x ↦ (f x) ^ n) z₀ := by
-
-  sorry
+  by_cases hn : 0 ≤ n
+  · exact zpow_nonneg h₁f hn
+  · rw [(Int.eq_neg_comm.mp rfl : n = - (- n))]
+    conv =>
+      arg 2
+      intro x
+      rw [zpow_neg]
+    exact AnalyticAt.inv (zpow_nonneg h₁f (by linarith)) (zpow_ne_zero (-n) h₂f)