Harmonic at a point

Remarks

Example: $f(x, y) = \log(x^2 + y^2)$ on $U = \R^2 \setminus \set{0}$ is harmonic at $a = (1, 0)$. Indeed, on $V = U$ one computes $\partial_x^2 f + \partial_y^2 f = \frac{2(y^2 - x^2)}{(x^2 + y^2)^2} + \frac{2(x^2 - y^2)}{(x^2 + y^2)^2} = 0$. Non-example: $f(x, y) = x^3$ on $\R^2$ is not harmonic at $(0, 0)$. Its Laplacian $6x$ vanishes at $(0, 0)$, but it is nonzero at points $(t, 0)$ with $t \ne 0$ arbitrarily close, so no neighbourhood $V$ works. A function is harmonic on $U$ if and only if it is harmonic at every point of $U$. In Mathlib the condition reads: $f$ is $C^2$ at $a$ and $\Delta f = 0$ on a neighbourhood of $a$. This is the same condition, since a function that is $C^2$ at a point is $C^2$ on a neighbourhood of it.