25 lines
797 B
Lean4
25 lines
797 B
Lean4
import Mathlib.Analysis.Meromorphic.Basic
|
||
|
||
open MeromorphicOn Metric Real Set Classical
|
||
|
||
variable
|
||
{𝕜 : Type*} [NontriviallyNormedField 𝕜]
|
||
{E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
|
||
{U : Set 𝕜} {f g : 𝕜 → E} {a : WithTop E} {a₀ : E}
|
||
|
||
/-- Derivatives of meromorphic functions are meromorphic. -/
|
||
@[fun_prop]
|
||
theorem meromorphicAt_deriv {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x) :
|
||
MeromorphicAt (deriv f) x := by
|
||
unfold MeromorphicAt at *
|
||
obtain ⟨n, hn⟩ := h
|
||
use n + 1
|
||
have := hn.deriv
|
||
sorry
|
||
|
||
/-- Logarithmic derivatives of meromorphic functions are meromorphic. -/
|
||
@[fun_prop]
|
||
theorem MeromorphicAt.logDeriv {f : 𝕜 → 𝕜} {x : 𝕜} (h : MeromorphicAt f x) :
|
||
MeromorphicAt (f⁻¹ * deriv f) x := by
|
||
sorry
|