Theorem: analyticAt_log (Ray/Analytic/HolomorphicUpstream.lean)

State before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
m : c ∈ Complex.slitPlane
⊢ AnalyticAt ℂ log c
Tactic:
rw [analyticAt_iff_eventually_differentiableAt]
State after:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
m : c ∈ Complex.slitPlane
⊢ ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ log z

State before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
m : c ∈ Complex.slitPlane
⊢ ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ log z
Tactic:
filter_upwards [Complex.isOpen_slitPlane.eventually_mem m]
State after:
case h
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
m : c ∈ Complex.slitPlane
⊢ ∀ a ∈ Complex.slitPlane, DifferentiableAt ℂ log a

State before:
case h
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
m : c ∈ Complex.slitPlane
⊢ ∀ a ∈ Complex.slitPlane, DifferentiableAt ℂ log a
Tactic:
intro z m
State after:
case h
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
m✝ : c ∈ Complex.slitPlane
z : ℂ
m : z ∈ Complex.slitPlane
⊢ DifferentiableAt ℂ log z

State before:
case h
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
m✝ : c ∈ Complex.slitPlane
z : ℂ
m : z ∈ Complex.slitPlane
⊢ DifferentiableAt ℂ log z
Tactic:
exact differentiableAt_id.clog m
State after:
no goals