Theorems · Theorem · potential theory

HarmonicAt.differentiableAt_complex_partial

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

Defined in: Mathlib.Analysis.Complex.Harmonic.Analytic
Cited by: 3 results in Mathlib
Foundations: Depth 245 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites57

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Realstatement and proof · cited by 25,697
RingHom.idstatement and proof · cited by 18,349
Complexstatement and proof · cited by 5,565
ContinuousLinearMapstatement and proof · cited by 5,352
mul_oneproof · cited by 3,885
one_mulproof · cited by 2,841
add_zeroproof · cited by 2,707
Nat.cast_oneproof · cited by 2,501
zero_addproof · cited by 2,366
Complex.ofRealstatement and proof · cited by 1,654
add_commproof · cited by 1,535

Cited by3

Results whose statement or proof uses this declaration.

InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eqproof · cited by 4
InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_univ_re_eqproof · cited by 1
HarmonicAt.analyticAt_complex_partialproof · cited by 0