LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-10-02

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 ball Poisson kernel is positive and has unit mass

Statement

Assume Countable Choice and $n \geq 3$ . For every ball $B_{R} (a)$ , interior point $x$ and boundary point $y$ , $P_{R, a} (x, y) > 0$ , and the kernel has total surface mass one: $\int_{\partial B_{R} (a)} P_{R, a} (x, y) d S_{y} = 1$ .

Facts & Assumptions

Given: Countable Choice, an integer $n \geq 3$ , a centre $a \in R^{n}$ , a radius $R > 0$ , an interior point $x \in B_{R} (a)$ and a boundary point $y \in \partial B_{R} (a)$ .

[F1]

For $x \in B_{R} (a)$ and $y \in \partial B_{R} (a)$ the ball Poisson kernel is $P_{R, a} (x, y) = (R^{2} - ∣ x - a ∣^{2}) / (R ω_{n - 1} ∣ x - y ∣^{n})$ , the negative outward boundary-slot normal derivative of the ball Green function, and it is a continuous function of $(x, y)$ on $B_{R} (a) \times \partial B_{R} (a)$ (Poisson kernel of a Euclidean ball).

[F2]

Let $Ω$ be a bounded $C^{1}$ domain carrying a Dirichlet Green function whose designated correctors satisfy $H_{y} \in C^{2} (\overline{Ω})$ ; let $P_{Ω} = - \partial_{ν_{y}} G_{Ω}$ . Then for every real $u \in C^{2} (\overline{Ω})$ and every $x \in Ω$ one has $u (x) = \int_{Ω} G_{Ω} (x, y) (- Δ u (y)) d y + \int_{\partial Ω} P_{Ω} (x, y) u (y) d S (y)$ , both integrals absolutely finite; moreover $P_{Ω} \geq 0$ on $Ω \times \partial Ω$ and $\int_{\partial Ω} P_{Ω} (x, y) d S (y) = 1$ for every $x \in Ω$ (Green representation for classical Poisson data).

[F3]

For $n \geq 3$ the ball $B_{R} (a)$ carries the Dirichlet Green function $G (x, z) = Φ (x - z) - (R / ∣ z - a ∣)^{n - 2} Φ (x - z^{*})$ (with the centre case $G (x, a) = Φ (x - a) - Φ (R)$ ), whose designated correctors all lie in $C^{2} (\overline{B_{R} (a)})$ , and whose negative outward boundary-slot normal derivative is the kernel of [F1] (Dirichlet Green function of a Euclidean ball, Poisson kernel of a Euclidean ball).

[F4]

$B_{R} (a)$ is a bounded $C^{1}$ domain (Euclidean balls are bounded C-one domains with radial outward normal).

[F5]

For $n \geq 1$ and $r > 0$ the sphere and ball measures are $∣ \partial B_{r} ∣ = ω_{n - 1} r^{n - 1}$ and $∣ B_{r} ∣ = ω_{n - 1} r^{n} / n$ , both finite and positive (Sphere and ball measures scale in Rn).

[F6]

Countable Choice ${A C}_{ω}$ is the standing hypothesis (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct

1.1givenF1F2F3F4F6

Work under [F6] and let $Ω : = B_{R} (a)$ . The hypotheses of [F2] are met: $Ω$ is a bounded $C^{1}$ domain by [F4], and by [F3] it carries a Dirichlet Green function whose designated correctors lie in $C^{2} (\overline{Ω})$ ; moreover the kernel $P_{R, a}$ of [F1] is by [F3] the negative boundary-slot normal derivative $P_{Ω}$ of that Green function, so the two notation systems denote the same function on $Ω \times \partial Ω$ .

2.1givenstep 1.1F1F5algebra

Strict positivity. By [F1], $P_{R, a} (x, y) = (R^{2} - ∣ x - a ∣^{2}) / (R ω_{n - 1} ∣ x - y ∣^{n})$ . Since $x$ lies in the open ball, $0 \leq ∣ x - a ∣ < R$ and the numerator $R^{2} - ∣ x - a ∣^{2}$ is positive; by [F5] both $R > 0$ and $ω_{n - 1} > 0$ , and $∣ x - y ∣ > 0$ because an interior point and a boundary point of $B_{R} (a)$ cannot coincide. A quotient of positive numbers is positive, so $P_{R, a} (x, y) > 0$ .

2.2givenstep 1.1F2F3algebra

Unit mass. Apply the representation identity of [F2] on $Ω = B_{R} (a)$ to the constant function $u \equiv 1$ , which is real and lies in $C^{2} (\overline{Ω})$ with $Δ u = 0$ : for every $x \in Ω$ , $1 = u (x) = \int_{Ω} G_{Ω} (x, y) \cdot 0 d y + \int_{\partial Ω} P_{Ω} (x, y) \cdot 1 d S (y)$ . Step 1.1 identifies $P_{Ω}$ with $P_{R, a}$ , and [F2] guarantees that the second integral is absolutely finite, so $\int_{\partial B_{R} (a)} P_{R, a} (x, y) d S_{y} = 1$ .

3.1step 2.1step 2.2F1F2∎

Step 2.1 gives $P_{R, a} (x, y) > 0$ for every interior $x$ and boundary $y$ , and step 2.2 gives unit total surface mass $\int_{\partial B_{R} (a)} P_{R, a} (x, y) d S_{y} = 1$ for every $x \in B_{R} (a)$ ; this proves both assertions of the statement. The argument uses the Green representation formula rather than the ball Dirichlet theorem, so the boundary-convergence question is not presupposed.

Depends on

Used by

Quantitative concentration of the ball Poisson kernel Example
Cap and complement estimate for the ball Poisson integral Lemma
Continuous Dirichlet problem on a ball Theorem
Harmonic functions are real analytic Theorem

Dependency tree · two levels

62 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)
Armin Schikorra, Partial Differential Equations I & II (2025) (standard reference, not scraped)
Sung-Jin Oh, Lecture Notes for Math 222A: Partial Differential Equations (2023) (standard reference, not scraped)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript) (standard reference, not scraped)