English
Let E be a real finite-dimensional inner product space and f: E → F. A function is harmonic at a point x if it is twice continuously differentiable near x and its Laplacian vanishes in a neighborhood of x.
Русский
Пусть E — вещественное конечномерное пространство с скалярным произведением, f: E → F. Функция гармонична в точке x, если она дважды непрерывно дифференцируема около x и её лапласиан равен нулю в некоторой окрестности x.
LaTeX
$$$\operatorname{HarmonicAt}(f,x) \iff \left( \operatorname{ContDiffAt}_{\mathbb{R}}^{2} f(x) \right) \land \left( \Delta f =_{nhds\ x} 0 \right)$$$
Lean4
/-- Let `E` be a real, finite-dimensional, inner product space and `x` be a point of `E`. A function `f`
on `E` is harmonic at `x` if it is two times continuously `ℝ`-differentiable and if its Laplacian
vanishes in a neighborhood of `x`.
-/
def HarmonicAt :=
(ContDiffAt ℝ 2 f x) ∧ (Δ f =ᶠ[𝓝 x] 0)
