Scout: AnalyticAt API for complex differentiable functions #
Key findings: #
- There is NO
DifferentiableAt.analyticAtin Mathlib. A singleDifferentiableAt ℂ g zdoes NOT suffice forAnalyticAt ℂ g z. You need differentiability in a neighborhood of z. - Key lemmas:
DifferentiableOn.analyticAt: DifferentiableOn ℂ f s → s ∈ 𝓝 z → AnalyticAt ℂ f zDifferentiable.analyticAt: Differentiable ℂ f → AnalyticAt ℂ f z (z is explicit)analyticAt_iff_eventually_differentiableAt: AnalyticAt ℂ f c ↔ ∀ᶠ z in 𝓝 c, DifferentiableAt ℂ f zAnalyticAt.differentiableAt: AnalyticAt 𝕜 f x → DifferentiableAt 𝕜 f xDifferentiableOn.analyticOnNhd: DifferentiableOn ℂ f s → IsOpen s → AnalyticOnNhd ℂ f sAnalyticOnNhd.deriv: AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 (deriv f) s [CompleteSpace]