How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
The negative Laplacian of the fundamental solution is the unit Dirac distribution
Statement
Assume Countable Choice and let . The locally integrable kernel of Fundamental solution for the positive operator minus Laplacian defines a regular distribution and satisfies . For every , the regular distribution associated with satisfies .
Facts & Assumptions
Given: Assume , let , and use the normalized kernel and its locally integrable representative.
Countable Choice, written , says every sequence of nonempty sets has a choice function; it is assumed by the kernel, surface-integration and Green-identity interfaces used here. (The Axiom of Countable Choice ()).
The kernel is for and for away from the pole; its value at zero may be assigned arbitrarily. (Fundamental solution for the positive operator minus Laplacian).
The normalized kernel is locally integrable for . (Local integrability of the Laplace fundamental kernel).
Under Countable Choice, the regular-functional map embeds modulo almost-everywhere equality into . (Locally integrable functions embed in distributions).
Distributional derivatives satisfy . (Distributional derivative).
The Dirac distribution is . (Dirac delta and its derivatives).
For real on a bounded domain, the second Green identity is , with outward normals. (Second Green identity).
For every , is compact and has graph charts near each point: has continuous coordinate partials with sum and power rules for one-variable derivatives, so the continuous-partials theorem gives the total derivative ; at one has , so is surjective and is a regular value of , and the regular-level graph theorem gives the local charts of . (For , every Euclidean closed ball and every Euclidean sphere of positive radius is compact, A regular level set is locally a graph of dimension , Regular and critical points, regular and critical values, and level sets, Submersions and immersions between Euclidean open sets, The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative, For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, Sums, scalar multiples, products and quotients: , , , and when , The Euclidean inner product on ).
For , set if and . Differentiation gives if and ; at , , the outward radial derivative is . (Fundamental solution for the positive operator minus Laplacian, Directional derivatives and partial derivatives of a map , The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, Continuity and derivatives of positive-base real powers).
If measurable functions converge almost everywhere and are dominated by one integrable function, their integrals converge. (Dominated convergence).
A test function is smooth and has compact support. (Test function space d of an open set).
For a test supported in a compact , its fixed-support derivative seminorms are finite; in particular its first and second derivatives are bounded. (Fixed support test function frechet space).
The Euclidean norm obeys the triangle and reverse triangle inequalities and is continuous. (The finite and reverse triangle inequalities for a norm; and for every norm on satisfies and is Lipschitz, hence continuous, for ).
A compact subset of is bounded. (A compact subset of a metric space is closed and bounded).
A bounded domain is a nonempty bounded open set whose boundary is locally a graph with the domain on one side; connectedness is not required. (Bounded C1 domains and their outward normals).
The kernel is smooth and harmonic away from its pole. (The Laplace fundamental solution is harmonic off its pole).
Translation of a distribution commutes with every constant-coefficient differential operator, and a fundamental solution translating gives . (Fundamental solution of a constant-coefficient operator).
Distributions are complex-linear functionals, with bilinear pairing and no conjugation. (Distribution).
Under Countable Choice, a singleton in is Lebesgue null. (A box with a degenerate side is Lebesgue null, and so is every coordinate hyperplane in ).
The regular distribution associated with a locally integrable function is defined by . (Regular distribution from a locally integrable function).
for the Euclidean metric. (Open ball, closed ball and sphere in a metric space, The Euclidean inner product on ).
Lebesgue measure is invariant under translations, including measurability of translates. (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation).
Integrals of integrable functions are invariant under measure-preserving maps. (Integral invariance under measure-preserving maps).
The translate convention is . (Translation of a function on ).
The Laplacian is the sum of the pure second coordinate derivatives. (The Laplacian of a function and of a vector field).
A measurable map preserves measure when for every measurable set . (Measure-preserving transformations and systems).
Under [A1], surface integration is defined for nonnegative Borel functions on a compact embedded hypersurface; monotonicity and homogeneity of the nonnegative integral show that a bounded continuous function is surface-integrable whenever the surface has finite area, with . (Surface integration on compact C1 hypersurfaces, Monotonicity and nonnegative homogeneity of the nonnegative integral).
For every the sphere has surface measure : the unit sphere has measure in the kernel convention, scaling by multiplies surface measure by , and ; in dimension two because , so . Combined with the radial derivative [F8], the normalized outward flux on every centered sphere is . (Fundamental solution for the positive operator minus Laplacian, Agreement with the existing polar sphere measure, The closed form for the volume of the unit -ball, The real Gamma functional equation ).
Proof
First take a real-valued test function . If its support is empty then and the desired pairing identity is immediate. Otherwise [F10] and [F13] let us choose with . For put . A point with radius strictly between and has a whole small ball in this set by [F12]; radial perturbations at either boundary sphere show by [F20]–[F21]. The point lies in it and it is bounded by . Near an outer-sphere point the inner-radius constraint is inactive and the annulus is the inside of that sphere; near an inner-sphere point the outer-radius constraint is inactive and the annulus is the outside of that sphere. The graph charts [F7], with a coordinate reflection when needed, therefore show that the annulus lies locally on one side of each graph. Its outward normals are on and on for , since the annulus lies inside the outer sphere and outside the inner sphere. Thus [F14] makes a bounded domain; connectedness is not required.
Let , where is the finite fixed-support seminorm from [F11]; then bounds . Since the outer radial derivative [F8] is constant on , the flux identity [F28] gives , so the sphere area is if and if . By [F27], the bounded continuous inner-boundary integrand is integrable. For , its absolute integral is at most ; for it is at most . Both bounds tend to zero as .
On , [F8] gives the outward radial derivative , and step 1.1 gives the annulus normal , so . The flux identity [F28] gives . By [F10] and [F27], the restriction of is surface-integrable. Therefore is the normalized spherical average of . Its difference from is at most , which tends to zero by continuity at the origin.
By [F15], is on a neighborhood of and there; [F10] gives the same regularity for . Apply [F6] with and . The outer-boundary terms vanish because the support lies strictly inside . On the inner sphere the normal is outward from the annulus. Hence .
Let , where is the finite fixed-support seminorm from [F11]; then bounds . For any sequence with , after discarding finitely many terms we have . The measurable functions then tend to zero off the null singleton and are dominated by , which is integrable by [F2]. Thus [F9] gives ; as this holds for every such sequence, the limit as is zero. The omitted integral of is bounded by , hence tends to zero and .
Taking in step 2.2 and using steps 1.2, 2.1 and 2.3 yields ; the integral over equals the one over because vanishes off the support. By [F2], [F3] and [F19], is the regular distribution; [F4] and [F25] identify the left side with , and [F5] identifies the right side with .
For a complex-valued test, apply step 3.1 separately to its real and imaginary parts and combine by complex linearity from [F17]. The pairing is bilinear, with no conjugation, as required by the distribution convention. Hence the identity holds for every test and .
For any fixed and test , put . It is integrable because it is bounded by a constant times on , which lies in a ball by [F12]–[F13]; use [F2] and [F11]. By [F22] and [F26], preserves Lebesgue measure; [F23] therefore gives , that is, . Thus the translate of is the regular distribution associated with , with the sign convention [F24]. Translate the identity in step 4.1: [F16] says constant-coefficient derivatives commute with translation and translates to , so . The proof handles and separately, excludes the distinct one-dimensional analogue by , includes the zero test and empty support, and is unchanged by the arbitrary value assigned to because a singleton is null [F18]. The choice cost is exactly [A1], inherited through the named measure and surface Green interfaces; no full Axiom of Choice is used. The statement is not an iff.
Source notes
Hunter §2.5 Theorem 2.23 and its proof give the second Green identity used on the punctured annulus; §2.6.1 gives the radial kernel, derivative and unit flux, and §2.6.2 states the distributional point-source interpretation. Hunter states that last interpretation but does not prove the test-function identity in this passage; steps 1.1–5.1 supply the excision argument, signs and limiting estimates. Teschl §5.3 equations (5.20)–(5.26) supplies the translated fundamental-solution and normalization conventions. Schmidt §2.2 uses the opposite sign, so only its convention comparison is retained; no exercise-class flux assertion is treated as proof.
Depends on
- Second Green identity
- For $n\ge1$, every Euclidean closed ball and every Euclidean sphere of positive radius is compact
- A regular level set is locally a $C^k$ graph of dimension $m-n$
- The closed form for the volume of the unit $n$-ball
- Directional derivatives and partial derivatives of a map $U\subseteq\mathbb{R}^m\to\mathbb{R}^n$
- Submersions and immersions between Euclidean open sets
- The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case
- Regular and critical points, regular and critical values, and level sets
- For a natural $n \ge 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $\iota(n)\,x^{\,n-1}$; for $n = 0$ it is the constant $1$, with derivative $0$; for a natural $n \ge 1$ the function $x \mapsto x^{-n}$ is differentiable at every $x \ne 0$ with derivative $-\iota(n)\,x^{-n-1}$; consequently every polynomial function is differentiable at every real, with the derivative computed term by term
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
- If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative
- The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t
- Continuity and derivatives of positive-base real powers
- Bounded C1 domains and their outward normals
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Distribution
- Distributional derivative
- Dirac delta and its derivatives
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- Euclidean spheres and closed balls as subspaces of $\mathbb{R}^n$
- Fixed support test function frechet space
- Fundamental solution of a constant-coefficient operator
- Fundamental solution for the positive operator minus Laplacian
- The Laplacian of a $C^2$ function and of a $C^2$ vector field
- Open ball, closed ball and sphere in a metric space
- Measure-preserving transformations and systems
- Regular distribution from a locally integrable function
- Test function space d of an open set
- Translation of a function on $\mathbb{R}^n$
- Surface integration on compact C1 hypersurfaces
- Agreement with the existing polar sphere measure
- The finite and reverse triangle inequalities for a norm; and for $n \ge 1$ every norm $N$ on $\mathbb{R}^n$ satisfies $N(x) \le C\lVert x\rVert_1$ and is Lipschitz, hence continuous, for $d_2$
- Local integrability of the Laplace fundamental kernel
- The Laplace fundamental solution is harmonic off its pole
- A box with a degenerate side is Lebesgue null, and so is every coordinate hyperplane in $\mathbb{R}^n$
- Monotonicity and nonnegative homogeneity of the nonnegative integral
- A compact subset of a metric space is closed and bounded
- Dominated convergence
- Integral invariance under measure-preserving maps
- Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation
- Locally integrable functions embed in distributions
- The real Gamma functional equation $\Gamma(s+1)=s\Gamma(s)$
Used by
Dependency tree · two levels
191 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- John K. Hunter, Notes on Partial Differential Equations (2014) (standard reference, not scraped)
- Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript) (standard reference, not scraped)
- Thomas Schmidt, Partial Differential Equations I (2026) (standard reference, not scraped)