63 lines
2.2 KiB
Lean4
63 lines
2.2 KiB
Lean4
import Mathlib.Analysis.Meromorphic.Basic
|
||
import Mathlib.Analysis.Calculus.Deriv.Mul
|
||
import Mathlib.Analysis.Calculus.Deriv.ZPow
|
||
import Mathlib.Analysis.Calculus.Deriv.Shift
|
||
|
||
open MeromorphicOn Metric Real Set Classical
|
||
|
||
theorem eventually_eventually_nhdsWithin₁
|
||
{α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop} [IsClosed s] :
|
||
(∀ᶠ (y : α) in nhdsWithin a s, ∀ᶠ (x : α) in nhds y, p x) ↔ ∀ᶠ (x : α) in nhdsWithin a s, p x := by
|
||
nth_rw 2 [← eventually_eventually_nhdsWithin]
|
||
constructor
|
||
· intro h
|
||
filter_upwards [h] with y hy
|
||
exact eventually_nhdsWithin_of_eventually_nhds hy
|
||
· intro h
|
||
filter_upwards [h] with y hy
|
||
have : y ∉ s := by sorry
|
||
rw [eventually_nhdsWithin_iff] at hy
|
||
rw [Filter.Eventually] at *
|
||
apply Filter.mem_of_superset hy
|
||
intro x hx
|
||
simp_all
|
||
sorry
|
||
|
||
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
|
||
|
||
rw [MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt] at h
|
||
obtain ⟨n, g, h₁g, h₂g⟩ := h
|
||
|
||
have : deriv (fun z ↦ (z - x) ^ n • g z)
|
||
=ᶠ[nhdsWithin x {x}ᶜ] fun z₀ ↦ (n * (z₀ - x) ^ (n - 1)) • g z₀ + (z₀ - x) ^ n • deriv g z₀ := by
|
||
have τ₀ : ∀ᶠ (y : 𝕜) in nhdsWithin x {x}ᶜ, AnalyticAt 𝕜 g y := by
|
||
exact eventually_nhdsWithin_of_eventually_nhds h₁g.eventually_analyticAt
|
||
have τ₁ : ∀ᶠ (y : 𝕜) in nhdsWithin x {x}ᶜ, y ≠ x := by
|
||
exact eventually_nhdsWithin_of_forall fun x_1 a ↦ a
|
||
filter_upwards [τ₀, τ₁] with z₀ h₁ h₂
|
||
rw [deriv_smul]
|
||
rw [add_comm]
|
||
congr
|
||
rw [deriv_comp_sub_const (f := fun z ↦ z ^ n)]
|
||
aesop
|
||
refine DifferentiableAt.zpow ?_ ?_
|
||
fun_prop
|
||
left
|
||
exact sub_ne_zero_of_ne h₂
|
||
fun_prop
|
||
|
||
have : deriv f =ᶠ[nhdsWithin x {x}ᶜ] (fun z ↦ (z - x) ^ n • g z) := by
|
||
sorry
|
||
|
||
apply MeromorphicAt.congr _ this.symm
|
||
fun_prop
|