Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-30
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 n≥2. The locally integrable kernel Φ of Fundamental solution for the positive operator minus Laplacian defines a regular distribution TΦ∈D′(Rn) and satisfies −ΔTΦ=δ0. For every y∈Rn, the regular distribution associated with x↦Φ(x−y) satisfies −ΔxTΦ(⋅−y)=δy.

Facts & Assumptions

Given: Assume ACω, let n≥2, and use the normalized kernel Φ and its locally integrable representative.

[A1]

Countable Choice, written ACω, 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 (ACω)).

[F1]

The kernel is ∣x∣2−n/((n−2)ωn−1) for n≥3 and −(2π)−1log⁡∣x∣ for n=2 away from the pole; its value at zero may be assigned arbitrarily. (Fundamental solution for the positive operator minus Laplacian).

[F2]

The normalized kernel is locally integrable for n≥2. (Local integrability of the Laplace fundamental kernel).

[F3]

Under Countable Choice, the regular-functional map embeds Lloc1 modulo almost-everywhere equality into D′. (Locally integrable functions embed in distributions).

[F4]

Distributional derivatives satisfy ⟨∂αu,φ⟩=(−1)∣α∣⟨u,∂αφ⟩. (Distributional derivative).

[F5]

The Dirac distribution is δa(φ)=φ(a). (Dirac delta and its derivatives).

[F6]

For real u,v∈C2(Ω‾) on a bounded C1 domain, the second Green identity is ∫Ω(vΔu−uΔv)=∫∂Ω(v∂νu−u∂νv) dS, with outward normals. (Second Green identity).

[F7]

For every r>0, Sr is compact and has C1 graph charts near each point: F(x)=⟨x,x⟩ has continuous coordinate partials ∂iF(x)=2xi with sum and power rules for one-variable derivatives, so the continuous-partials theorem gives the total derivative DF(x)h=2⟨x,h⟩; at x∈Sr=F−1(r2) one has DF(x)x=2r2≠0, so DF(x) is surjective and r2 is a regular value of F, and the regular-level graph theorem gives the local C1 charts of Sr. (For n≥1, every Euclidean closed ball and every Euclidean sphere of positive radius is compact, A regular level set is locally a Ck graph of dimension m−n, 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 n≥1 the function x↦xn is differentiable everywhere with derivative ι(n) x n−1; for n=0 it is the constant 1, with derivative 0; for a natural n≥1 the function x↦x−n is differentiable at every x≠0 with derivative −ι(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), (αf)′(c)=αf′(c), (fg)′(c)=f′(c)g(c)+f(c)g′(c), and (f/g)′(c)=(f′(c)g(c)−f(c)g′(c))/g(c)2 when g(c)≠0, The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn).

[F8]

For r>0, set qn(r)=r2−n/((n−2)ωn−1) if n≥3 and q2(r)=−(2π)−1log⁡r. Differentiation gives qn′(r)=−1/(ωn−1rn−1) if n≥3 and q2′(r)=−1/(2πr); at x=rω, ∣ω∣=1, the outward radial derivative is DωΦ(x)=qn′(r). (Fundamental solution for the positive operator minus Laplacian, Directional derivatives and partial derivatives of a map U⊆Rm→Rn, 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).

[F9]

If measurable functions converge almost everywhere and are dominated by one integrable function, their integrals converge. (Dominated convergence).

[F10]

A test function is smooth and has compact support. (Test function space d of an open set).

[F11]

For a test supported in a compact K, its fixed-support derivative seminorms are finite; in particular its first and second derivatives are bounded. (Fixed support test function frechet space).

[F13]

A compact subset of Rn is bounded. (A compact subset of a metric space is closed and bounded).

[F14]

A bounded C1 domain is a nonempty bounded open set whose boundary is locally a C1 graph with the domain on one side; connectedness is not required. (Bounded C1 domains and their outward normals).

[F15]

The kernel is smooth and harmonic away from its pole. (The Laplace fundamental solution is harmonic off its pole).

[F16]

Translation of a distribution commutes with every constant-coefficient differential operator, and a fundamental solution translating δ0 gives δy. (Fundamental solution of a constant-coefficient operator).

[F17]

Distributions are complex-linear functionals, with bilinear pairing and no conjugation. (Distribution).

[F18]

Under Countable Choice, a singleton in Rn is Lebesgue null. (A box with a degenerate side is Lebesgue null, and so is every coordinate hyperplane in Rn).

[F19]

The regular distribution associated with a locally integrable function is defined by ⟨Tf,φ⟩=∫fφ. (Regular distribution from a locally integrable function).

[F20]

Sr={x:∣x∣=r} and B‾r={x:∣x∣≤r}. (Euclidean spheres and closed balls as subspaces of Rn).

[F22]

Lebesgue measure is invariant under translations, including measurability of translates. (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation).

[F23]

Integrals of integrable functions are invariant under measure-preserving maps. (Integral invariance under measure-preserving maps).

[F24]

The translate convention is (τyf)(x)=f(x−y). (Translation of a function on Rn).

[F25]

The Laplacian is the sum of the pure second coordinate derivatives. (The Laplacian of a C2 function and of a C2 vector field).

[F26]

A measurable map preserves measure when μ(T−1E)=μ(E) for every measurable set E. (Measure-preserving transformations and systems).

[F27]

Under [A1], surface integration is defined for nonnegative Borel functions on a compact embedded C1 hypersurface; monotonicity and homogeneity of the nonnegative integral show that a bounded continuous function is surface-integrable whenever the surface has finite area, with ∫S∣g∣ dS≤sup⁡S∣g∣∫S1 dS. (Surface integration on compact C1 hypersurfaces, Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F28]

For every r>0 the sphere Sr has surface measure ∣Sr∣=ωn−1rn−1: the unit sphere has measure ωn−1=∣Sn−1∣ in the kernel convention, scaling by r multiplies surface measure by rn−1, and ∣Sn−1∣=n∣B1∣; in dimension two ∣B1∣=V2(1)=π because Γ(2)=1, so ω1=∣S1∣=2π. Combined with the radial derivative [F8], the normalized outward flux on every centered sphere is −∫Sr∂νΦ dS=−qn′(r)∫Sr1 dS=1. (Fundamental solution for the positive operator minus Laplacian, Agreement with the existing polar sphere measure, The closed form for the volume of the unit n-ball, The real Gamma functional equation Γ(s+1)=sΓ(s)).

Proof

technique · direct
1.1A1givenF7F10F12F13F14F20F21cases

First take a real-valued test function φ. If its support is empty then φ=0 and the desired pairing identity is immediate. Otherwise [F10] and [F13] let us choose R>0 with supp⁡φ⊂BR(0). For 0<ε<min⁡{1,R} put Ωε={z:ε<∣z∣<R}. A point with radius strictly between ε and R has a whole small ball in this set by [F12]; radial perturbations at either boundary sphere show ∂Ωε=Sε∪SR by [F20]–[F21]. The point ((R+ε)/2,0,…,0) lies in it and it is bounded by R. 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 C1 graph. Its outward normals are +ω on SR and −ω on Sε for ω=x/∣x∣, since the annulus lies inside the outer sphere and outside the inner sphere. Thus [F14] makes Ωε a bounded C1 domain; connectedness is not required.

1.2A1F1F8F28F11F27casesalgebra

Let C1:=n p1(φ), where p1 is the finite fixed-support seminorm from [F11]; then C1 bounds ∣Dφ∣. Since the outer radial derivative [F8] is constant on Sε, the flux identity [F28] gives −qn′(ε)∫Sε1 dS=1, so the sphere area is ωn−1εn−1 if n≥3 and 2πε if n=2. By [F27], the bounded continuous inner-boundary integrand is integrable. For n≥3, its absolute integral is at most εC1/(n−2); for n=2 it is at most ε∣log⁡ε∣C1. Both bounds tend to zero as ε↓0.

2.1A1F28F8F10F27step 1.1

On Sε, [F8] gives the outward radial derivative qn′(ε), and step 1.1 gives the annulus normal −ω, so ∂νannΦ=cε:=−qn′(ε)>0. The flux identity [F28] gives cε∫Sε1 dS=1. By [F10] and [F27], the restriction of φ is surface-integrable. Therefore ∫Sεφ ∂νannΦ dS is the normalized spherical average of φ. Its difference from φ(0) is at most sup⁡∣z∣=ε∣φ(z)−φ(0)∣, which tends to zero by continuity at the origin.

2.2A1F6F10F15step 1.1

By [F15], Φ is C2 on a neighborhood of Ωε‾ and ΔΦ=0 there; [F10] gives the same regularity for φ. Apply [F6] with u=Φ and v=φ. The outer-boundary terms vanish because the support lies strictly inside BR(0). On the inner sphere the normal is outward from the annulus. Hence −∫ΩεΦΔφ dz=∫Sε(φ ∂νannΦ−Φ ∂νannφ) dS.

2.3F2F9F11F18step 1.1algebra

Let C2:=n p2(φ), where p2 is the finite fixed-support seminorm from [F11]; then C2 bounds ∣Δφ∣. For any sequence εj→0 with εj>0, after discarding finitely many terms we have εj<1. The measurable functions gj=∣Φ∣1Bεj then tend to zero off the null singleton {0} and are dominated by ∣Φ∣1B1, which is integrable by [F2]. Thus [F9] gives ∫Bεj∣Φ∣→0; as this holds for every such sequence, the limit as ε↓0 is zero. The omitted integral of ΦΔφ is bounded by C2∫Bε∣Φ∣, hence tends to zero and ∫ΩεΦΔφ→∫BRΦΔφ.

3.1F2F3F4F5F19F25step 2.2step 1.2step 2.1step 2.3

Taking ε↓0 in step 2.2 and using steps 1.2, 2.1 and 2.3 yields −∫RnΦ(z)Δφ(z) dz=φ(0); the integral over Rn equals the one over BR because Δφ vanishes off the support. By [F2], [F3] and [F19], TΦ is the regular distribution; [F4] and [F25] identify the left side with ⟨−ΔTΦ,φ⟩, and [F5] identifies the right side with ⟨δ0,φ⟩.

4.1F4F5F17step 3.1cases

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 −ΔTΦ=δ0.

5.1F2F11F12F13F16F18F22F23F24F26A1step 4.1cases∎

For any fixed y∈Rn and test φ, put h(z)=Φ(z)φ(z+y). It is integrable because it is bounded by a constant times ∣Φ∣ on supp⁡φ−y, which lies in a ball by [F12]–[F13]; use [F2] and [F11]. By [F22] and [F26], T−y(x)=x−y preserves Lebesgue measure; [F23] therefore gives ∫h(T−yx) dx=∫h(z) dz, that is, ∫Φ(x−y)φ(x) dx=∫Φ(z)φ(z+y) dz. Thus the translate of TΦ is the regular distribution associated with x↦Φ(x−y), with the sign convention [F24]. Translate the identity in step 4.1: [F16] says constant-coefficient derivatives commute with translation and δ0 translates to δy, so −ΔxTΦ(⋅−y)=δy. The proof handles n=2 and n≥3 separately, excludes the distinct one-dimensional analogue by n≥2, includes the zero test and empty support, and is unchanged by the arbitrary value assigned to Φ(0) 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

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