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.

Bounded compact data give an everywhere finite Newtonian potential

Statement

Assume Countable Choice and let $n \geq 2$ . Suppose the $L^{\infty} (R^{n})$ class $f$ has a finite-valued measurable representative $f_{0}$ with compact support $K$ . Then the Newtonian-potential integral for $f_{0}$ is absolutely finite at every $x \in R^{n}$ , and $N f_{0}$ is locally bounded. If $g$ is any finite-valued measurable representative with $g = f_{0}$ almost everywhere, then its integral is also absolutely finite at every $x$ and equals $N f_{0} (x)$ pointwise.

Facts & Assumptions

Given: Assume ${A C}_{ω}$ , let $n \geq 2$ , and let $f_{0}$ be a finite-valued measurable representative of an $L^{\infty} (R^{n})$ class, with compact support $K$ .

[A1]

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

[F1]

An $L^{\infty}$ function is measurable and has finite essential supremum. (The space $L^{\infty} (μ)$ of essentially bounded measurable functions).

[F2]

If its essential supremum is finite, then $∣ f_{0} ∣ \leq ∥ f_{0} ∥_{\infty}$ almost everywhere. (The essential supremum is attained as the least essential bound).

[F3]

The positive-minus-Laplacian kernel is given by its radial power or logarithmic formula away from zero, and its value at zero may be assigned arbitrarily. (Fundamental solution for the positive operator minus Laplacian).

[F4]

The Newtonian potential is the integral $\int_{R^{n}} Φ (x - y) f_{0} (y) d y$ wherever it is absolutely finite. (Newtonian potential of compactly supported data).

[F5]

The normalized kernel $Φ$ is locally integrable on $R^{n}$ . (Local integrability of the Laplace fundamental kernel).

[F6]

Local integrability means that the absolute integral on every Euclidean ball of positive radius is finite. (A locally integrable function on $R^{n}$ ).

[F7]

Under ${A C}_{ω}$ , a $C^{1}$ diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions. (A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions).

[F8]

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

[F9]

For $n \geq 1$ , $∥ \cdot ∥_{2}$ is a norm on $R^{n}$ , so it satisfies the triangle inequality. (The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ , Each $∥ \cdot ∥_{p}$ is a norm on $R^{n}$ , and the induced metrics are exactly $d_{1}$ , $d_{2}$ and $d_{\infty}$ of the published metric-spaces page).

[F10]

The determinant of a triangular matrix is the product of its diagonal entries. (The determinant of a triangular matrix is the product of its diagonal entries).

[F11]

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

[F12]

A nonnegative measurable function has zero integral over a measurable null set. (A nonnegative integral over a null set vanishes).

[F13]

The integral over a measurable set is the integral after multiplying by its indicator. (Integral over a measurable subset).

[F14]

The $L^{1}$ class is a vector space and its integral is linear. (The Lebesgue integral is linear on $L^{1} (μ)$ ).

[F15]

A continuous map pulls back Borel sets to Borel sets. (A continuous map has Borel preimages of Borel sets).

[F16]

Products, sums, differences and absolute values of measurable real-valued functions are measurable. (Arithmetic and lattice operations preserve measurability whenever they are defined).

[F17]

A real measurable function is integrable exactly when its absolute value has finite integral, and its integral is the difference of the integrals of its positive and negative parts. (Integrable real and complex functions, and their integrals).

[F18]

$B (c, r) = {y : ∥ y - c ∥ < r}$ for $r > 0$ . (Open ball, closed ball and sphere in a metric space).

[F19]

A $C^{1}$ diffeomorphism is a bijection between open sets whose map and inverse are $C^{1}$ . ( $C^{k}$ Euclidean maps and diffeomorphisms).

[F20]

Under ${A C}_{ω}$ , every Borel subset of $R^{n}$ is Lebesgue measurable. (Assuming countable choice, every Borel subset of $R^{n}$ is Lebesgue measurable).

[F21]

Under ${A C}_{ω}$ , a $C^{1}$ diffeomorphism maps Lebesgue measurable sets to Lebesgue measurable sets. (A C^1 diffeomorphism maps Lebesgue measurable sets to Lebesgue measurable sets).

[F22]

Almost-everywhere equality means equality off a measurable null set. (Measure-null sets and almost-everywhere statements relative to a measure).

[F23]

The nonnegative integral is homogeneous for nonnegative scalars, including the zero scalar case. (Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F24]

For $n \geq 1$ , the Euclidean norm and published metric satisfy $∥ x - y ∥_{2} = d_{2} (x, y)$ . (Each $∥ \cdot ∥_{p}$ is a norm on $R^{n}$ , and the induced metrics are exactly $d_{1}$ , $d_{2}$ and $d_{\infty}$ of the published metric-spaces page).

Proof

technique · direct

1.1F1F2F8F16F22givencases

Put $M : = ∥ f_{0} ∥_{\infty} < \infty$ . By [F2] and [F22], there is a measurable null set $E$ outside which $∣ f_{0} ∣ \leq M$ . Define $\hat{f} = f_{0} 1_{E^{c}}$ . By [F16], $\hat{f}$ is measurable, and $∣ \hat{f} ∣ \leq M$ everywhere; it vanishes outside $K$ . The set $K$ is closed and Borel by [F8]. If $K = \emptyset$ , then $f_{0} = 0$ everywhere and the conclusion is immediate, so assume $K \neq \emptyset$ .

1.2F8F9F10F15F18F19F24givenalgebra

Fix a ball $C = B (c, R_{C})$ with $R_{C} > 0$ . By [F8], choose $p \in R^{n}$ and $R_{K} > 0$ with $K \subset B (p, R_{K})$ . Put $R : = 1 + R_{C} + ∥ c - p ∥_{2} + R_{K} > 0$ . For $x \in C$ and $y \in K$ , the norm triangle inequality [F9] applied to $x - y = (x - c) + (c - p) + (p - y)$ gives $∥ x - y ∥_{2} < R$ . By [F24] and the ball definition [F18], this yields $x - K \subset B (0, R)$ . For a fixed $x$ , define $T_{x} (y) = x - y$ . Directly, $T_{x} (T_{x} (y)) = y$ , $D T_{x} = - I_{n}$ , and $∣ \det D T_{x} ∣ = 1$ by [F10]. Thus $T_{x}$ is a $C^{1}$ diffeomorphism by [F19]. Moreover, $x - K = T_{x}^{- 1} (K)$ is Borel by [F15] and [F8].

2.1A1F3F5F6F7F11F13F16F20F21step 1.2algebra

Choose the finite pole value $0$ in [F3]. Since $T_{x}^{- 1} = T_{x}$ , [F21] shows that preimages under $T_{x}$ of Lebesgue measurable sets are Lebesgue measurable; hence $y \mapsto Φ (x - y)$ is measurable. The set $x - K$ is Borel by step 1.2, so [F20] and [F16] make $h_{x} (z) : = 1_{x - K} (z) ∣ Φ (z) ∣$ nonnegative Lebesgue measurable. Applying [F7] to $h_{x}$ and $T_{x}$ , with $∣ \det D T_{x} ∣ = 1$ , gives $\int_{x - K} ∣ Φ (z) ∣ d z = \int_{R^{n}} h_{x} (z) d z = \int_{R^{n}} h_{x} (T_{x} (y)) d y = \int_{K} ∣ Φ (x - y) ∣ d y,$ because $x - y \in x - K$ exactly when $y \in K$ . By [F13], [F11] and step 1.2, $\int_{K} ∣ Φ (x - y) ∣ d y \leq \int_{B (0, R)} ∣ Φ (z) ∣ d z < \infty,$ where finiteness follows from [F5]–[F6]. This holds uniformly for $x \in C$ .

3.1F1F4F11F16F17F23step 2.1algebra

Since $\hat{f}$ vanishes off $K$ and $∣ \hat{f} ∣ \leq M$ , pointwise $∣ Φ (x - y) \hat{f} (y) ∣ \leq M 1_{K} (y) ∣ Φ (x - y) ∣$ . The translated kernel and $\hat{f}$ are measurable by step 2.1 and [F1, F16], so $u_{x}$ is measurable. Monotonicity [F11] and homogeneity [F23], together with step 2.1, show $\int_{R^{n}} ∣ Φ (x - y) \hat{f} (y) ∣ d y \leq M \int_{K} ∣ Φ (x - y) ∣ d y \leq M \int_{B (0, R)} ∣ Φ (z) ∣ d z < \infty$ for every $x \in C$ . By [F17], $u_{x} \in L^{1}$ and $\int u_{x} = \int u_{x}^{+} - \int u_{x}^{-}$ with both terms finite and nonnegative, so $∣ N \hat{f} (x) ∣ \leq \int ∣ u_{x} ∣$ . The bound is uniform on $C$ . Taking $C = B (x, 1)$ for each $x$ proves absolute finiteness everywhere and local boundedness.

4.1F4F12F13F14F16F17F22step 2.1step 3.1algebra

Let $g$ be any finite-valued measurable representative with $g = f_{0}$ almost everywhere. By [F22] choose a measurable null set $N_{g}$ outside which $g = f_{0}$ , and put $E^{'} : = E \cup N_{g}$ . For fixed $x$ , the integrands $u_{g} (y) : = Φ (x - y) g (y)$ and $u_{\hat{f}} (y) : = Φ (x - y) \hat{f} (y)$ agree off $E^{'}$ , so $d : = u_{g} - u_{\hat{f}}$ vanishes there. By [F13], $\int ∣ d ∣ = \int_{E^{'}} ∣ d ∣ = 0$ using [F12]. Hence $d \in L^{1}$ ; step 3.1 gives $u_{\hat{f}} \in L^{1}$ , and [F14] gives $u_{g} = u_{\hat{f}} + d \in L^{1}$ with $\int u_{g} = \int u_{\hat{f}}$ . The measurability established in step 2.1 and [F16] justify the products and difference. Thus every such representative has the same pointwise potential value and absolute finiteness.

5.1A1F3F4F5F6F7F20F21step 1.1step 3.1step 4.1cases∎

If $M = 0$ , step 1.1 gives $\hat{f} = 0$ and step 4.1 gives zero potential for every representative. The case $n = 1$ is excluded by the hypothesis $n \geq 2$ . Countable Choice is used exactly through the kernel convention, local-integrability, Borel-measurability, measurable-set, and change-of-variables interfaces [F3–F7, F20–F21]; no full Axiom of Choice is used. There are no endpoint claims or biconditional cases.

Source notes

Schmidt §2.11, printed p.70, defines the Newton potential for $f \in L_{c p t}^{\infty}$ and says the integral is finite because the fundamental solution lies in $L_{l o c}^{1}$ ; his kernel $F$ has the opposite sign to the present $Φ$ , which does not affect absolute convergence. The proof above derives the uniform bound and representative independence from the stated local-integrability and measure interfaces. Hunter §2.6.1, printed p.33, states local integrability of the normalized kernel, while §2.7 equation (2.24), printed p.36, names the integral the Newtonian potential after proving the smooth compact-data case. Hunter's passage does not itself prove the present everywhere-finite bounded-data claim; that part is established here.

Depends on

Used by

Dependency tree · two levels

115 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

Thomas Schmidt, Partial Differential Equations I (2026) (standard reference, not scraped)
John K. Hunter, Notes on Partial Differential Equations (2014) (standard reference, not scraped)