Analyticity of Harmonic Functions

If f : ℂ → ℝ is harmonic at x, we show that ∂f/∂1 - I • ∂f/∂I is complex-analytic at x.

TODO: As soon as PR https://github.com/leanprover-community/mathlib4/issues/9598 (feat(Analysis/Complex): HasPrimitives on disc) is merged, extend this to show that f itself is locally the real part of a holomorphic function, and hence real-analytic.

theorem HarmonicAt.differentiableAt_complex_partial {f : ℂ → ℝ} {x : ℂ} (hf : InnerProductSpace.HarmonicAt f x) : DifferentiableAt ℂ (fun (z : ℂ) => ↑((fderiv ℝ f z) 1) - Complex.I * ↑((fderiv ℝ f z) Complex.I)) x

If f : ℂ → ℝ is harmonic at x, then ∂f/∂1 - I • ∂f/∂I is complex differentiable at x.

theorem HarmonicAt.analyticAt_complex_partial {f : ℂ → ℝ} {x : ℂ} (hf : InnerProductSpace.HarmonicAt f x) : AnalyticAt ℂ (fun (z : ℂ) => ↑((fderiv ℝ f z) 1) - Complex.I * ↑((fderiv ℝ f z) Complex.I)) x

If f : ℂ → ℝ is harmonic at x, then ∂f/∂1 - I • ∂f/∂I is complex analytic at x.