Theorems · Theorem · potential theory

HarmonicAt.analyticAt_complex_partial

∀ {f : ℂ → ℝ} {x : ℂ},
  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.

Defined in

Mathlib.Analysis.Complex.Harmonic.Analytic

Cited by

0 results in Mathlib

Foundations

Depth 286 from the axioms · uses propext, Classical.choice, Quot.sound