AcceptedTheorem · Statement with omitted proof

Fundamental solutions of the Laplacian

The logarithmic kernel in two dimensions and inverse-distance kernel in three dimensions are fundamental solutions of the negative Laplacian.

Larsson & Thomée ↗
Theorem 3.5 · printed p. 31

Download Lean file ↓

Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

The logarithmic kernel in two dimensions and inverse-distance kernel in three dimensions are fundamental solutions of the negative Laplacian.

U(x)=\begin{cases}-\dfrac1{2\pi}\log|x|,&d=2,\\[3pt]\dfrac1{4\pi|x|},&d=3.\end{cases}

Assumptions & context

The Euclidean domain has dimension two or three, with the distributional fundamental-solution condition defined using test functions.

Source

Larsson & Thomée. Partial differential equations with numerical methods.

Theorem 3.5 · printed p. 31

02 / LEAN REPRESENTATION

Formal statement

Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.

theorem thm_3_5 (d : ℕ) (hd : d = 2 ∨ d = 3) : IsFundamentalSolutionPoisson d (U d) := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm35

/-- The operator of Poisson's equation (3.3): `-Δφ = -∑_{j=1}^d ∂²φ/∂x_j²`, built from
classical partial derivatives. It is applied only to smooth test functions. -/
def negLaplacian {d : ℕ} (φ : Euclidean d → ℝ) (x : Euclidean d) : ℝ :=
  -∑ j : Fin d, partialDeriv (partialDeriv φ j) j x

/-- `U` is a fundamental solution for Poisson's equation (3.3), i.e. `-ΔU = δ` in the sense of
distributions. `U` is locally integrable, so it defines a distribution, and
`∫ U (-Δφ) dx = φ(0)` for every smooth compactly supported real test function `φ` on `ℝ^d`. -/
def IsFundamentalSolutionPoisson (d : ℕ) (U : Euclidean d → ℝ) : Prop :=
  LocallyIntegrable U volume ∧
  ∀ φ : Euclidean d → ℝ, ContDiff ℝ (⊤ : ℕ∞) φ → HasCompactSupport φ →
    (∫ x, U x * negLaplacian φ x) = φ 0

/-- The function `U` of Theorem 3.5. For `d = 2` it is `-(1/(2π)) log|x|`, and for `d = 3` it is
`1/(4π|x|)`. The theorem only concerns `d = 2, 3`, so the value for other `d` is irrelevant.
At `x = 0` Lean's totalized `log` and division give the value `0`. This is a single point of
measure zero, so it does not affect the distributional statement. -/
def U : (d : ℕ) → Euclidean d → ℝ
  | 2, x => -(1 / (2 * Real.pi)) * Real.log ‖x‖
  | 3, x => 1 / (4 * Real.pi * ‖x‖)
  | _, _ => 0

/-- Larsson–Thomée, Theorem 3.5: `U` is a fundamental solution for Poisson's equation (3.3)
when `d = 2` or `d = 3`. -/
theorem thm_3_5 (d : ℕ) (hd : d = 2 ∨ d = 3) : IsFundamentalSolutionPoisson d (U d) := by
  sorry

end PDETextbook.LarssonThomee.Thm35

How to read the formalization

The distributional formulation gives meaning to the singular kernel at the origin.

← Back to all statements