Scout: AnalyticAt API for complex differentiable functions

Key findings:

• There is NO DifferentiableAt.analyticAt in Mathlib. A single DifferentiableAt ℂ g z does NOT suffice for AnalyticAt ℂ g z. You need differentiability in a neighborhood of z.
• Key lemmas:
  • DifferentiableOn.analyticAt : DifferentiableOn ℂ f s → s ∈ 𝓝 z → AnalyticAt ℂ f z
  • Differentiable.analyticAt : Differentiable ℂ f → AnalyticAt ℂ f z (z is explicit)
  • analyticAt_iff_eventually_differentiableAt : AnalyticAt ℂ f c ↔ ∀ᶠ z in 𝓝 c, DifferentiableAt ℂ f z
  • AnalyticAt.differentiableAt : AnalyticAt 𝕜 f x → DifferentiableAt 𝕜 f x
  • DifferentiableOn.analyticOnNhd : DifferentiableOn ℂ f s → IsOpen s → AnalyticOnNhd ℂ f s
  • AnalyticOnNhd.deriv : AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 (deriv f) s [CompleteSpace]