54 lines
2.3 KiB
Lean4
54 lines
2.3 KiB
Lean4
import Mathlib
|
||
|
||
open MeromorphicOn Real Set Classical Topology
|
||
|
||
variable
|
||
{𝕜 : Type*} [NontriviallyNormedField 𝕜]
|
||
{E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
|
||
{X : Type*} {x : X} [TopologicalSpace X]
|
||
|
||
theorem eventually_nhdsWithin_eventually_nhds_iff_of_isOpen {s : Set X} {a : X} {p : X → Prop}
|
||
(hs : IsOpen s) : (∀ᶠ y in 𝓝[s] a, ∀ᶠ x in 𝓝 y, p x) ↔ ∀ᶠ x in 𝓝[s] a, p x := by
|
||
nth_rw 2 [← eventually_eventually_nhdsWithin]
|
||
constructor
|
||
· intro h
|
||
filter_upwards [h] with _ hy
|
||
exact eventually_nhdsWithin_of_eventually_nhds hy
|
||
· intro h
|
||
filter_upwards [h, eventually_nhdsWithin_of_forall fun _ a ↦ a] with _ _ _
|
||
simp_all [IsOpen.nhdsWithin_eq]
|
||
|
||
@[simp]
|
||
theorem eventually_nhdsNE_eventually_nhds_iff [T1Space X] {a : X} {p : X → Prop} :
|
||
(∀ᶠ y in 𝓝[≠] a, ∀ᶠ x in 𝓝 y, p x) ↔ ∀ᶠ x in 𝓝[≠] a, p x :=
|
||
eventually_nhdsWithin_eventually_nhds_iff_of_isOpen isOpen_ne
|
||
|
||
theorem Filter.EventuallyEq.nhdsNE_deriv {f f₁ : 𝕜 → E} {x : 𝕜} (h : f₁ =ᶠ[𝓝[≠] x] f) :
|
||
deriv f₁ =ᶠ[𝓝[≠] x] deriv f := by
|
||
rw [Filter.EventuallyEq, ← eventually_nhdsNE_eventually_nhds_iff] at *
|
||
filter_upwards [h] with y hy
|
||
apply Filter.EventuallyEq.deriv hy
|
||
|
||
/--
|
||
Derivatives of meromorphic functions are meromorphic.
|
||
-/
|
||
@[fun_prop]
|
||
protected theorem MeromorphicAt.deriv [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x) :
|
||
MeromorphicAt (deriv f) x := by
|
||
rw [MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt] at h
|
||
obtain ⟨n, g, h₁g, h₂g⟩ := h
|
||
have : _root_.deriv (fun z ↦ (z - x) ^ n • g z)
|
||
=ᶠ[𝓝[≠] x] fun z ↦ (n * (z - x) ^ (n - 1)) • g z + (z - x) ^ n • _root_.deriv g z := by
|
||
filter_upwards [eventually_nhdsWithin_of_eventually_nhds h₁g.eventually_analyticAt,
|
||
eventually_nhdsWithin_of_forall fun _ a ↦ a] with z₀ h₁ h₂
|
||
rw [deriv_smul (DifferentiableAt.zpow (by fun_prop) (by simp_all [sub_ne_zero_of_ne h₂]))
|
||
(by fun_prop), add_comm, deriv_comp_sub_const (f := (· ^ n))]
|
||
aesop
|
||
rw [MeromorphicAt.meromorphicAt_congr (Filter.EventuallyEq.nhdsNE_deriv h₂g),
|
||
MeromorphicAt.meromorphicAt_congr this]
|
||
sorry
|
||
|
||
theorem MeromorphicAt.order_deriv [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x) (h₂ : h.order ≠ 0) :
|
||
h.deriv.order = h.order -1 := by
|
||
sorry
|