kebekus/aristotle
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Update Basic.lean
Some checks failed
Lean Action CI / build (push) Has been cancelled
Details

Browse Source
This commit is contained in:
Stefan Kebekus
2025-11-04 16:30:01 +01:00
parent b3f99c37f2
commit 2bb8762a4f
1 changed files with 2 additions and 15 deletions
Download Patch File Download Diff File Expand all files Collapse all files

17
Aristotle/Basic.lean
View File

@@ -7,20 +7,7 @@ variable
{𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
/-- Derivatives of meromorphic functions are meromorphic. -/ /-- Derivatives of meromorphic functions are meromorphic. -/
@[fun_prop] theorem meromorphicAt_deriv_of_order_eq_top {f : 𝕜 → 𝕜} {x : 𝕜}
theorem meromorphicAt_deriv {f : 𝕜 → 𝕜} {x : 𝕜} (h : MeromorphicAt f x) (h₁ : h.order = ⊤) :
(h : MeromorphicAt f x) (h₁ : h.order ≠ ⊤) :
MeromorphicAt (deriv f) x := by MeromorphicAt (deriv f) x := by
obtain ⟨g, h₁g, h₂g, h₃⟩ := h.order_ne_top_iff.1 h₁
lift h.order to ℤ using h₁ with n hn
have : (n : WithTop ℤ).untop₀ = n := by
sorry
simp_all [this]
have : deriv f =ᶠ[nhdsWithin x {x}ᶜ] deriv (fun z ↦ (z - x) ^ n * g z) := by
sorry
have : deriv f =ᶠ[nhdsWithin x {x}ᶜ] fun z ↦ n * (z - x) ^ (n - 1) * g z + (z - x) ^ n * deriv g z := by
sorry
apply MeromorphicAt.congr _ this.symm
sorry sorry