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.

A bounded-domain Dirichlet Green function is unique and positive

Statement

Assume Countable Choice and $n \geq 2$ . Let $Ω \subseteq R^{n}$ be bounded, nonempty, open and connected, and suppose a Dirichlet Green function as in Dirichlet Green function for minus Laplacian exists. Then it is unique and $G_{Ω} (x, y) > 0$ for every distinct $x, y \in Ω$ . No boundary differentiability is needed, and existence is not asserted.

Facts & Assumptions

Given: The objects and hypotheses in the statement, the kernel $Φ$ fixed by Fundamental solution for the positive operator minus Laplacian, and correctors supplied by the Green-function definition.

[A1]

Countable Choice, written ${A C}_{ω}$ , is an assumption of the Green and kernel conventions used here (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

For each pole, the Green definition supplies a corrector $H_{y} \in C^{2} (Ω) \cap C (\overline{Ω})$ with boundary values $H_{y} (z) = Φ (z - y)$ and $G_{Ω} (x, y) = Φ (x - y) - H_{y} (x)$ away from the pole (Dirichlet Green function for minus Laplacian).

[F2]

The kernel is $Φ (x) = ∣ x ∣^{2 - n} / ((n - 2) ω_{n - 1})$ for $n \geq 3$ and $Φ (x) = - (2 π)^{- 1} \log ∣ x ∣$ for $n = 2$ , with $ω_{n - 1} > 0$ (Fundamental solution for the positive operator minus Laplacian).

[F3]

A real $C^{2}$ function on a bounded open set that is continuous on its closure and has $Δ u \geq 0$ has its closure maximum on the boundary (Weak maximum principle for the laplacian).

[F4]

If instead $Δ u \leq 0$ , its closure minimum is on the boundary (Weak minimum principle for the laplacian).

[F5]

For every $η > 0$ there is an integer $N \geq 1$ with $1 / N < η$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[F6]

Positive reciprocals reverse strict order: $0 < a < b$ implies $0 < b^{- 1} < a^{- 1}$ (Inverses of positives are positive, and reciprocation reverses order).

[F7]

The natural logarithm is strictly increasing and onto $R$ , and $\log (1 / s) = - \log s$ for $s > 0$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[F8]

Positive real powers obey the quotient and exponent laws (The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents).

[F9]

If $n \geq 2$ , deleting one point from a nonempty connected open subset of $R^{n}$ leaves a nonempty, open, connected, path-connected set (Puncturing a connected open subset of $R^{n}$ preserves path-connectedness for $n \geq 2$ ).

[F10]

A harmonic function on a connected domain that attains a global maximum or minimum in the domain is constant (Strong maximum principle for harmonic functions).

[F11]

For fixed $y$ , $G_{Ω} (\cdot, y)$ is harmonic away from $y$ , extends continuously to $\overline{Ω} ∖ {y}$ , and has zero boundary trace (Dirichlet Green function for minus Laplacian).

[F12]

Mathematical induction applies to properties of natural numbers (The principle of mathematical induction).

[F13]

The order on $R$ makes it a totally ordered field (The reals form a totally ordered field).

[F14]

Positive elements of an ordered field are closed under multiplication; in particular, a product of nonnegative reals is nonnegative (Ordered field, The reals form a totally ordered field).

[F15]

The Laplacian of a $C^{2}$ function is the sum of its pure second partial derivatives (The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field).

[F17]

A $C^{2}$ function is harmonic exactly when its Laplacian is zero (The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field).

[F16]

Total derivatives obey sum and scalar rules, and their coordinate partials are obtained by applying them to standard basis vectors; applying these facts twice gives linearity of each second partial of $C^{2}$ functions (Sums and scalar multiples of totally differentiable maps are totally differentiable with the expected derivatives, A total derivative computes every directional derivative, and its matrix is the Jacobian).

Proof

technique · direct

1.1F1F3F4F15F16F17givenalgebra

Suppose $G$ and $\tilde{G}$ are two Green functions with correctors $H_{y}$ and ${\tilde{H}}_{y}$ . For fixed $y$ , $w = H_{y} - {\tilde{H}}_{y}$ is $C^{2}$ , and [F15]–[F16] give $Δ w = Δ H_{y} - Δ {\tilde{H}}_{y} = 0$ , so it is harmonic by [F17]; it is continuous on $\overline{Ω}$ and zero on $\partial Ω$ . The weak maximum principle [F3] gives $w \leq 0$ , and the weak minimum principle [F4] gives $w \geq 0$ . Hence $w = 0$ and $G (x, y) = \tilde{G} (x, y)$ for all $x \neq y$ . This holds for every pole, proving uniqueness.

1.2F1givenchoose

Fix $y \in Ω$ . Continuity of $H_{y}$ at $y$ gives $r_{0} > 0$ and $M = ∣ H_{y} (y) ∣ + 1$ such that $∣ H_{y} (x) ∣ \leq M$ whenever $∣ x - y ∣ < r_{0}$ ; shrink $r_{0}$ if needed so ${\overline{B}}_{2} (y, r_{0}) \subset Ω$ .

1.3F2F5F6F8F12F13F14algebrachoose

Suppose $n \geq 3$ , put $m = n - 2 \geq 1$ and $C = 1 / ((n - 2) ω_{n - 1}) > 0$ . For $0 < r < 1$ , induction on $k \in N$ for the property $0 < r^{k + 1} \leq r$ starts with equality at $k = 0$ ; if it holds at $k$ , then $r^{k + 2} = r^{k + 1} r > 0$ and $r^{k + 1} - r^{k + 2} = r^{k + 1} (1 - r) \geq 0$ by [F13, F14], so it holds at $k + 1$ . Thus [F12] gives $r^{m} \leq r$ . By [F8], $r^{2 - n} = r^{- m} = 1 / r^{m} \geq 1 / r$ . Given $L > 0$ , [F5] with $η = C / L$ gives $N \geq 1$ with $1 / N < C / L$ ; [F6] then gives $N > L / C$ . Thus $0 < r < \min {1, 1 / N}$ implies $Φ (r) = C r^{- m} \geq C / r > C N > L$ . This proves $Φ (r) \to + \infty$ as $r ↓ 0$ for every $n \geq 3$ .

1.4F2F5F6F7algebrachoose

Suppose $n = 2$ and put $C = 1 / (2 π) > 0$ . For any $L > 0$ , surjectivity in [F7] gives $s_{0} > 0$ with $\log s_{0} > L / C$ . Apply [F5] to $1 / s_{0}$ and then [F6] to obtain an integer $N > s_{0}$ . Whenever $0 < r < 1 / N$ , [F6] gives $1 / r > N > s_{0}$ , so [F7] yields $Φ (r) = C \log (1 / r) > C \log s_{0} > L$ . Hence $Φ (r) \to + \infty$ as $r ↓ 0$ in dimension two as well.

2.1F1step 1.2step 1.3step 1.4algebrachoose

By steps 1.3 and 1.4, choose $0 < r_{y} < r_{0}$ so that $Φ (x - y) > M$ whenever $0 < ∣ x - y ∣ \leq r_{y}$ . Then $G_{Ω} (x, y) = Φ (x - y) - H_{y} (x) > 0$ on that punctured closed ball. This is the local strict positivity near the pole.

3.1F4F11step 2.1givencases

Let $x \in Ω$ with $∣ x - y ∣ > r_{y}$ and choose $0 < ε < \min {r_{y}, ∣ x - y ∣}$ . The set $D = Ω ∖ {\overline{B}}_{2} (y, ε)$ is bounded, open, and contains $x$ . A point outside $\partial Ω \cup S_{2} (y, ε)$ has a neighborhood either contained in $D$ or disjoint from $D$ , so $\partial D \subseteq \partial Ω \cup S_{2} (y, ε)$ . By [F11], $G_{Ω} (\cdot, y)$ is harmonic on $D$ and continuous on $\overline{D}$ . Its boundary values are zero on $\partial Ω$ and positive on $S_{2} (y, ε)$ by step 2.1. The weak minimum principle [F4] therefore gives $G_{Ω} (x, y) \geq 0$ . Points with $0 < ∣ x - y ∣ \leq r_{y}$ already have strict positivity by step 2.1, so $G_{Ω} (\cdot, y) \geq 0$ throughout $Ω ∖ {y}$ .

4.1F9F10F11F15F16F17step 2.1step 3.1assume-contracontradictiondischarge-contradictionalgebra

By [F9], $Ω ∖ {y}$ is a connected open set. The Green function is harmonic there by [F11], so its negative is harmonic by [F15]–[F17]. Step 3.1 gives $G_{Ω} \geq 0$ there. Assume it vanishes at some $x \neq y$ [assume-contra]. Then $- G_{Ω} (\cdot, y)$ attains its global maximum $0$ at that interior point. By [F10] it is constant on the punctured domain, contradicting the strict positivity near $y$ from step 2.1. Therefore $G_{Ω} (x, y) > 0$ whenever $x \neq y$ [contradiction, discharge-contradiction].

5.1A1F1F2F5step 1.3step 1.4cases∎

The argument treats $n = 2$ and all $n \geq 3$ separately, excludes $n = 1$ and dimension zero by the hypothesis, and makes no boundary smoothness or existence claim. Countable Choice is retained exactly because the preceding Green and kernel conventions assume it; the maximum principles and puncture argument add no choice principle, and the pointwise thresholds use only the Archimedean property. There is no iff assertion.

Source notes

Teschl §5.4 Theorem 5.21, printed p.124, establishes uniqueness for the classical Dirichlet problem. Lemma 5.23, printed pp.126–127, assumes a bounded connected domain, proves Green positivity by using the blow-up at the pole and a strong minimum principle, and notes that connectedness is required for positivity. The proof here derives the power/log blow-up and punctured-domain connectedness explicitly; it uses weak minimum on the bounded punctured domains and the strong maximum principle on $Ω ∖ {y}$ .

Schmidt §2.8 remarks (2)–(3), printed pp.44–45, derives uniqueness from uniqueness of the harmonic corrector and the weak maximum principle, then derives nonpositivity under $Δ F = δ_{0}$ . Here $Φ = - F$ , so that sign comparison supports nonnegativity only; strict positivity is proved above.

Depends on

Used by

An isolated boundary point obstructs pointwise-zero Green data Counterexample

Dependency tree · two levels

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