DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-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.

Poisson kernel from a Dirichlet Green function

Definition

Assume the Axiom of Countable Choice, written ${A C}_{ω}$ , and let $n \geq 2$ . Let $Ω \subset R^{n}$ be a bounded $C^{1}$ domain carrying a Dirichlet Green function $G_{Ω}$ for $- Δ$ . For every pole $p \in Ω$ , assume its designated corrector satisfies $H_{p} \in C^{2} (\overline{Ω})$ , as required by the Green-symmetry hypothesis.

For $x \in Ω$ and $y \in \partial Ω$ , define the boundary-slot normal derivative by $\partial_{ν_{y}} G_{Ω} (x, y) : = D_{z} (Φ (z - x) - H_{x} (z)) ∣_{z = y} \cdot ν_{Ω} (y),$ and define the Poisson kernel by $P_{Ω} (x, y) : = - \partial_{ν_{y}} G_{Ω} (x, y) .$ Here $Φ$ is the positive-minus-Laplacian fundamental solution fixed in Dirichlet Green function for minus Laplacian, and $ν_{Ω}$ is the published outward unit normal. The derivative in the boundary variable is the trace from interior points, not a derivative of a function initially defined on $\partial Ω$ .

Facts & Assumptions

Given: ${A C}_{ω}$ , $n \geq 2$ , the bounded $C^{1}$ domain $Ω$ , its Dirichlet Green function, and the correctors $H_{p} \in C^{2} (\overline{Ω})$ for every $p \in Ω$ .

[A1]

The Axiom of Countable Choice is written ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). The Green definition, bounded- $C^{1}$ /surface convention, and Green-symmetry theorem carry this same assumption (Dirichlet Green function for minus Laplacian, Bounded C1 domains and their outward normals, Symmetry of the Dirichlet Green function). Here its substantive role is exactly the symmetry step 3.1, which identifies the slots; the collar geometry and normal-trace calculation require no further choice.

[F1]

For each pole $x$ , $G_{Ω} (z, x) = Φ (z - x) - H_{x} (z)$ for interior $z \neq x$ (Dirichlet Green function for minus Laplacian).

[F2]

The Green-symmetry hypothesis requires $H_{x} \in C^{2} (\overline{Ω})$ for every pole $x$ (Symmetry of the Dirichlet Green function).

[F3]

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

[F4]

Under the stated hypotheses, $G_{Ω} (x, z) = G_{Ω} (z, x)$ for all distinct interior points (Symmetry of the Dirichlet Green function).

[F5]

A bounded $C^{1}$ domain is a bounded open set with locally $C^{1}$ graph boundary and its published outward unit normal (Bounded C1 domains and their outward normals).

[F6]

A positive-radius Euclidean sphere is the level set $F^{- 1} (r^{2})$ of $F (z) = ⟨ z - x, z - x ⟩$ : the coordinate partials $\partial_{i} F (z) = 2 (z_{i} - x_{i})$ are continuous, so the total derivative is $D F (z) h = 2 ⟨ z - x, h ⟩$ , and $D F (z) (z - x) = 2 r^{2} \neq 0$ at every $z \in S_{2} (x, r)$ ; hence $r^{2}$ is a regular value of $F$ . (Euclidean spheres and closed balls as subspaces of $R^{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 \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 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)$ , $(f g)^{'} (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) \neq 0$ , The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[F7]

Regular level sets are locally $C^{1}$ graphs (A regular level set is locally a $C^{k}$ graph of dimension $m - n$ ).

[F8]

For a $C^{1}$ function up to a bounded $C^{1}$ boundary, the classical normal derivative is its boundary gradient dotted with the outward unit normal (Classical normal derivative).

Verification

1.1givenF5F6F7choosealgebra

Fix $x \in Ω$ . Openness gives $r > 0$ with ${\overline{B}}_{2} (x, 2 r) \subset Ω$ . Set $D_{r} = Ω ∖ {\overline{B}}_{2} (x, r)$ . It is bounded and open, its boundary is the disjoint union of $\partial Ω$ and $S_{2} (x, r)$ , and the latter is a regular level set, hence locally a $C^{1}$ graph by [F6]–[F7]. The outer boundary retains the $C^{1}$ charts from [F5]. The point $x + \frac{3}{2} r e_{1}$ belongs to $D_{r}$ , so $D_{r}$ is nonempty; connectedness is not required in the bounded $C^{1}$ convention. Therefore $D_{r}$ is a bounded $C^{1}$ domain.

2.1F1F2F3step 1.1algebra

On ${\overline{D}}_{r}$ , the formula [F1] expresses $G_{Ω} (z, x)$ as $Φ (z - x) - H_{x} (z)$ . The closure of $D_{r}$ stays away from $x$ ; [F2] and the off-pole smoothness in [F3] therefore give a $C^{2}$ extension of this function to ${\overline{D}}_{r}$ . In particular, its first derivative has a continuous boundary trace on the outer component $\partial Ω$ .

3.1A1F1F2F3F4step 2.1algebra

For every interior $z \in D_{r}$ , [F4] identifies $G_{Ω} (x, z)$ with $G_{Ω} (z, x)$ . Thus the first-variable derivative of the right-hand expression in [F1] gives the unique continuous trace of the derivative in the second variable of $G_{Ω} (x, z)$ as $z$ approaches $y \in \partial Ω$ . The assumption [A1] is inherited from the Green definition and the bounded- $C^{1}$ /surface convention; its only substantive use here is [F4], through the Green-symmetry theorem, to identify the slots. The collar regularity is pointwise and choice-free. No full Axiom of Choice is used.

4.1

Restricting $G_{Ω} (\cdot, x)$ to $D_{r}$ meets the hypotheses of the published classical normal derivative in [F8]. On the outer boundary its outward normal is $ν_{Ω}$ , since the excised sphere lies strictly inside $Ω$ . The formula in the Definition is therefore exactly the classical outward normal derivative trace, and it is independent of the chosen sufficiently small $r$ . The minus sign fixes the positive-kernel convention. No Sobolev trace or conormal derivative is asserted. [F5, F8, step 1.1, step 2.1, step 3.1, algebra] $□$

Source notes

Teschl §5.4, equation (5.35), printed p. 125, defines the Poisson kernel as the negative outward normal derivative of the Green function in its second variable. Equation (5.34) expresses that Green function as the fundamental solution minus a harmonic corrector; the stated $C^{2} (\overline{Ω})$ regularity makes the boundary trace used here classical. Schmidt §2.8, printed pp. 45–46, gives the Green-symmetry hypothesis and representation formula. Schmidt uses the opposite Laplacian/Green sign convention; translating to $- Δ$ and the positive Green function yields the same negative-outward-derivative convention. These citations support the definition; the interior-slot trace is identified from the explicitly stated local symmetry hypothesis.

Depends on

Used by

Dependency tree · two levels

88 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

Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript) (standard reference, not scraped)
Thomas Schmidt, Partial Differential Equations I (2026) (standard reference, not scraped)