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.
Fundamental solution for the positive operator minus Laplacian
Statement
Assume Countable Choice and . With in the published chart/polar convention, set for and for , . Extend it as a locally integrable function at the pole. The one-dimensional analogue is ; the subsequent Green theory does not silently include it.
Definition
The kernel candidate for the operator is Its value at may be assigned arbitrarily; the resulting measurable function is interpreted through its locally integrable class. Here is the chart surface measure, which agrees with the polar measure . In dimension one put . This fixes the positive-minus-Laplacian sign convention; the later distributional theorem proves for .
Facts & Assumptions
Given: Assume , let , and use the published chart/polar convention for surface measure and Lebesgue polar coordinates. The one-dimensional profile is considered separately.
Countable Choice, written , says every sequence of nonempty sets has a choice function. (The Axiom of Countable Choice ()).
The chart surface measure agrees with the polar measure and satisfies . (Agreement with the existing polar sphere measure).
Every Euclidean ball of positive radius has positive finite Lebesgue measure under Countable Choice. (Euclidean balls have positive finite Lebesgue measure).
The unit ball volume is , hence in dimension two. (The closed form for the volume of the unit -ball).
For nonnegative Borel , polar integration gives . (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma).
A distribution is a fundamental solution of a constant-coefficient operator when . (Fundamental solution of a constant-coefficient operator).
A locally integrable function defines the regular functional . (Regular distribution from a locally integrable function).
Distributional second derivatives act by the signed test derivative formula. (Distributional derivative).
The Dirac distribution satisfies . (Dirac delta and its derivatives).
The Laplacian is the divergence of the gradient, with . (The Laplacian of a function and of a vector field).
Under Countable Choice, every singleton in is Lebesgue null. (A box with a degenerate side is Lebesgue null, and so is every coordinate hyperplane in ).
Proof
By [F1] and [F2], is finite and strictly positive. In dimension two, [F3] gives , so and the logarithmic coefficient in the Statement is exactly . The operator sign is using the definition [F9]. This uses the Countable Choice assumption [A1] through the measure convention.
In dimension one, , so is locally integrable. For a test , [F7] gives . The slopes of are to the left of zero and to the right; integrating by parts separately on the two half-lines, the compact-support endpoint terms vanish and , so the negative integral equals by [F8]. Thus and [F5] identifies it as the one-dimensional fundamental-solution analogue for .
Let . For , [F4] gives . For , using from step 1.1, it gives . The polar integration use [F4] also assumes [A1].
The formulas are continuous away from zero, so they are integrable on every compact set avoiding the pole. Step 2.1 proves integrability in a neighborhood of the pole; hence . By [F10], changing its value at the single point zero does not change its almost-everywhere class, and [F6] defines the corresponding regular functional.
The zero-dimensional case is outside the stated kernel and has no unit-sphere convention used here. The polar endpoint is included as an improper integral in step 2.1; away from zero the kernel is smooth. Countable Choice is used only through [F1], [F2], and [F4]; no full Axiom of Choice is used.
Source notes
Hunter §2.6 equations (2.12)–(2.13), printed p. 33; Teschl §5.3 equations (5.22)–(5.26), printed pp. 117–118. The one-dimensional formula is checked directly by its slope jump; for the distributional Dirac identity is proved later rather than assumed in this definition.
Depends on
Fundamental solution of a constant-coefficient operator
The polar surface set function on the unit sphere
Agreement with the existing polar sphere measure
The Axiom of Countable Choice ()
Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma
Euclidean balls have positive finite Lebesgue measure
The closed form for the volume of the unit -ball
Regular distribution from a locally integrable function
Distributional derivative
Dirac delta and its derivatives
The Laplacian of a function and of a vector field
A box with a degenerate side is Lebesgue null, and so is every coordinate hyperplane in