diff --git a/Nevanlinna/analyticAt.lean b/Nevanlinna/analyticAt.lean index 2b4ffc3..87731af 100644 --- a/Nevanlinna/analyticAt.lean +++ b/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) diff --git a/lake-manifest.json b/lake-manifest.json index b0837ec..ae6cb22 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "325d06c3ef6bcb16c43c4ac6614976731ce6a63e", + "rev": "b100ff2565805e9f30a482788b3fc66937a7f38a", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5dfdc66e0d503631527ad90c1b5d7815c86a8662", + "rev": "de91b59101763419997026c35a41432ac8691f15", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ac7b989cbf99169509433124ae484318e953d201", + "rev": "b0b73e5bc33f1bc4d3c0f254630dd0e262cecc08", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "b8570f16d4170663edb8a12b8eae9f0d84e96ab4", + "rev": "e3d7d7f053ea862ffb7d1613eff6de0f2e3e8e14", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,