Fundamental solutions of the Laplacian

TheoremThe Newtonian kernel is harmonic away from the origin#●ready to prove

Let \(m > 2\) be a natural number. The function \(x \mapsto 1/|x|^{m-2}\) on the Euclidean space \(\mathbb{R}^m\), where \(|x|\) is the Euclidean norm, is harmonic on \(\mathbb{R}^m \setminus \{0\}\).

public theorem_wanted harmonicOnNhd_one_div_norm_pow_sub_two
    {m : ℕ} (hm : 2 < m) : InnerProductSpace.HarmonicOnNhd
  (fun x : EuclideanSpace ℝ (Fin m) => 1 / ‖x‖ ^ (m - 2)) ({0}ᶜ)
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of several variables), problem ma_proofbench_l1_81.

TheoremThe logarithm of the norm is harmonic on the punctured plane#●ready to prove

The function \(g(x) = \log|x|\), where \(|x|\) is the Euclidean norm of \(x \in \mathbb{R}^2\), is harmonic on \(\mathbb{R}^2 \setminus \{0\}\): near every point \(x \ne 0\) it is twice continuously differentiable and its Laplacian vanishes.

public theorem_wanted harmonicOnNhd_log_norm_euclideanSpace_two
    : InnerProductSpace.HarmonicOnNhd (fun x : EuclideanSpace ℝ (Fin 2) => Real.log ‖x‖) ({0}ᶜ)
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functions of a complex variable; Geometric function theory), problem ma_proofbench_l1_50.

TheoremFundamental solution of the Laplacian in dimension three#●ready to prove

Let \(E\) be a real inner product space of dimension \(3\). Then there is a complex-valued tempered distribution \(N\) on \(E\) such that \(\Delta N = \delta_0\), where \(\Delta\) is the Laplacian in the sense of distributions and \(\delta_0\) is the Dirac delta at the origin.

public theorem_wanted exists_fundamental_solution_laplacian
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    (hdim : Module.finrank ℝ E = 3) :
    ∃ N : 𝓢'(E, ℂ), Δ N = TemperedDistribution.delta (0 : E)
Sources
  • L. Evans, Partial Differential Equations, §2.2.

TheoremThe Newton potential is harmonic away from the origin#●ready to prove

Let \(E\) be a real inner product space of dimension \(3\), and define \(N : E \to \mathbb{R}\) by \(N(y) = -1/(4\pi\|y\|)\) for \(y \neq 0\) and \(N(0) = 0\). Then the Laplacian of \(N\) vanishes at every point \(x \neq 0\) of \(E\).

public theorem_wanted newton_potential_harmonic
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    (hdim : Module.finrank ℝ E = 3) (x : E) (hx : x ≠ 0) :
    (Δ (fun (y : E) => (-((4 * Real.pi * ‖y‖))⁻¹ : ℝ)) : E → ℝ) x = 0
Sources
  • L. Evans, Partial Differential Equations, §2.2.
4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.