LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 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.

Local integrability of the Laplace fundamental kernel

Statement

Assume Countable Choice and $n \geq 2$ . The normalized Laplace kernel $Φ$ is locally integrable on $R^{n}$ : its singularity is $\log ∣ x ∣$ for $n = 2$ and $∣ x ∣^{2 - n}$ for $n \geq 3$ . It therefore defines a regular distribution.

Facts & Assumptions

Given: Assume ${A C}_{ω}$ and let $n \geq 2$ . Write $ω_{n - 1} = ∣ S^{n - 1} ∣$ in the chart/polar convention and take the normalized kernel from Fundamental solution for the positive operator minus Laplacian.

[A1]

Countable Choice, written ${A C}_{ω}$ , says every sequence of nonempty sets has a choice function. (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

For $n \geq 3$ , $Φ (x) = ∣ x ∣^{2 - n} / ((n - 2) ω_{n - 1})$ ; for $n = 2$ , $Φ (x) = - (2 π)^{- 1} \log ∣ x ∣$ , for $x \neq 0$ . (Fundamental solution for the positive operator minus Laplacian).

[F2]

Polar integration gives the integral of a nonnegative Borel function as the radial integral against $r^{n - 1} d r d σ$ . (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma).

[F3]

The chart surface measure equals the polar measure and $ω_{n - 1} = n ∣ B_{1} ∣$ . (Agreement with the existing polar sphere measure).

[F4]

Every Euclidean ball of positive radius has positive finite Lebesgue measure. (Euclidean balls have positive finite Lebesgue measure).

[F5]

The nonnegative integral is monotone under pointwise order. (Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F6]

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

[F7]

Every Borel subset of $R^{n}$ is Lebesgue measurable under Countable Choice. (Assuming countable choice, every Borel subset of $R^{n}$ is Lebesgue measurable).

[F8]

A locally integrable function defines the regular functional $⟨ u_{Φ}, φ ⟩ = \int Φ φ$ , which depends only on its almost-everywhere class. (Regular distribution from a locally integrable function).

[F9]

Under Countable Choice, the regular-functional map from $L_{l o c}^{1}$ modulo almost-everywhere equality takes values in $D^{'}$ . (Locally integrable functions embed in distributions).

[F10]

Under Countable Choice, every singleton in $R^{n}$ is Lebesgue null. (Every at most countable subset of $R^{n}$ is Lebesgue null; in particular $λ_{1} (Q) = 0$ ).

[F11]

The kernel's value at zero may be assigned arbitrarily; the resulting measurable function is interpreted through its locally integrable class. (Fundamental solution for the positive operator minus Laplacian).

Proof

technique · direct

1.1F3F4

By [F3] and [F4], $ω_{n - 1} = n ∣ B_{1} ∣$ is positive and finite in every stated dimension.

2.1F1F2F3F11step 1.1

For $n \geq 3$ and any $R > 0$ , assign the finite value $0$ to the kernel at the pole as permitted by [F11]; then $∣ Φ ∣ 1_{B_{R}}$ is Borel. Apply [F2] and use [F1] and $σ (S^{n - 1}) = ω_{n - 1}$ from [F3] to obtain $\int_{B_{R}} ∣ Φ (x) ∣ d x = \frac{1}{(n - 2) ω_{n - 1}} \int_{0}^{R} r^{n - 1} r^{2 - n} ω_{n - 1} d r = \frac{R^{2}}{2 (n - 2)} < \infty .$

2.2F1F2F3F11step 1.1casesalgebra

For $n = 2$ and any $R > 0$ , again assign $Φ (0) = 0$ as permitted by [F11]. By [F1]–[F3] and step 1.1, $\int_{B_{R}} ∣ Φ (x) ∣ d x = \frac{ω_{1}}{2 π} \int_{0}^{R} r ∣ \log r ∣ d r .$ If $0 < R \leq 1$ , the radial integral is $- \frac{R^{2}}{2} \log R + \frac{R^{2}}{4}$ ; if $R \geq 1$ , splitting at $1$ gives $\frac{R^{2}}{2} \log R - \frac{R^{2}}{4} + \frac{1}{2}$ . Both values are finite, including at $R = 1$ , and the prefactor is finite by step 1.1.

3.1F1F5F6F7F8step 2.1step 2.2algebra

Let $K \subset R^{n}$ be compact. By [F6], $K$ is closed and bounded, hence Borel and Lebesgue measurable by [F7]; boundedness and the Euclidean triangle inequality give a centered ball $B_{R}$ containing $K$ . By [F5] and steps 2.1–2.2, $\int_{K} ∣ Φ ∣ \leq \int_{B_{R}} ∣ Φ ∣ < \infty$ (and the empty $K$ has integral zero). Since [F1] and [F11] make $Φ$ measurable, this is $Φ \in L_{l o c}^{1} (R^{n})$ by [F8]'s definition.

4.1A1F2F3F4F7F8F9F10F11step 2.1step 2.2step 3.1cases∎

The regular functional in [F8] is therefore well-defined; [F9], under [A1], proves it is a distribution. The pole value changes only a singleton, which is null by [F10], and the radial integrals prove finiteness at the improper endpoint $r = 0$ and every finite outer radius $R > 0$ . The claim assumes $n \geq 2$ ; it makes no global-integrability assertion at $R = \infty$ , and Countable Choice is used only through the named polar, surface-measure, ball-measure, Borel-measurability, singleton-null, and embedding interfaces, not full AC.

Source notes

Hunter §2.6.1, printed p.33, states local integrability of the normalized fundamental solution after giving its radial formula; the same passage notes that second derivatives, with size $∣ x ∣^{- n}$ , are not locally integrable. Teschl §5.3 equations (5.25)–(5.26), printed pp.117–118, likewise records $Φ \in L_{l o c}^{1}$ and the different behavior of its second derivatives. The present proof computes the kernel's radial integrals rather than using the source's stated conclusion. The preceding kernel definition also contains this local integrability calculation because it must make the kernel extension meaningful before the current dependency level; this lemma retains its separate promised result and supplies the explicit distribution interface.

Depends on

Used by

Dependency tree · two levels

70 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)