LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)

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.

Uniqueness for harmonic functions on a punctured half-space with zero trace, decaying at the pole and at infinity

Statement

Let $H : = {x \in R^{3} : x_{3} > 0}$ be the open upper half-space, let $a > 0$ and $p : = a e_{3} \in H$ , where $e_{3} : = (0, 0, 1)$ . Let $w : \overline{H} ∖ {p} \to R$ be a function (closure as in Interior, closure, boundary, limit point, isolated point and dense subset of a metric space) with:

(i) $w$ is continuous (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form) on $\overline{H} ∖ {p}$ and of class $C^{2}$ with $Δ w = 0$ on $H ∖ {p}$ (The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field, $C^{k}$ Euclidean maps and diffeomorphisms);

(ii) $w = 0$ on $\partial H = {x_{3} = 0}$ ;

(iii) $∣ x - p ∣ w (x) \to 0$ as $x \to p$ , $x \neq p$ ;

(iv) $w (x) \to 0$ as $∣ x ∣ \to \infty$ within $H$ : for every $ε > 0$ there is $R > 0$ with $∣ w (x) ∣ \leq ε$ for all $x \in H ∖ {\overline{B}}_{R} (0)$ .

Then $w = 0$ on $H ∖ {p}$ .

The conclusion is a uniqueness statement for the stated class only: no removable-singularity theorem, no pole condition beyond the sub-Coulomb growth (iii), no boundary regularity of $\partial H$ beyond the flat graph, and no claim about $w$ outside $H$ are asserted.

Facts & Assumptions

Given: The open upper half-space $H = {x_{3} > 0}$ , the point $p = a e_{3}$ with $a > 0$ , and a function $w : \overline{H} ∖ {p} \to R$ satisfying (i)-(iv) of the statement. Write $B_{r} (q)$ for the open ball and use the Euclidean norm and metric on $R^{3}$ .

[F1]

The weak maximum principle: if $Ω \subseteq R^{n}$ , $n \geq 2$ , is bounded, nonempty and open and $u \in C^{2} (Ω) \cap C (\overline{Ω})$ satisfies $Δ u \geq 0$ on $Ω$ , then $\max_{\overline{Ω}} u = \max_{\partial Ω} u$ (Weak maximum principle for the laplacian).

[F2]

A $C^{2}$ function is harmonic where $Δ u = 0$ ; $Δ$ is defined as the sum of the pure second partial derivatives, is linear on $C^{2}$ functions and annihilates constants (The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field, $C^{k}$ Euclidean maps and diffeomorphisms).

[F3]

For $n = 3$ the fundamental solution is $Φ (x) = ∣ x ∣^{- 1} / ω_{2}$ with $ω_{2} > 0$ , and for every pole $q$ the function $x \mapsto Φ (x - q)$ is smooth and harmonic on $R^{3} ∖ {q}$ ; the function $b_{q} (x) : = ∣ x - q ∣^{- 1} = ω_{2} Φ (x - q)$ is therefore a positive constant multiple of a harmonic function, hence $C^{\infty}$ and harmonic off $q$ , and it is continuous wherever it is defined (Fundamental solution for the positive operator minus Laplacian, The Laplace fundamental solution is harmonic off its pole, The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field).

[F4]

An open ball is open, its closure is the corresponding closed ball, and $x \mapsto ∣ x - q ∣$ is continuous for the Euclidean metric; the reciprocal $t \mapsto 1 / t$ is continuous on $t > 0$ ; a function with $∣ x - q ∣ \geq δ > 0$ on its domain has $∣ b_{q} (x) - b_{q} (y) ∣ \leq ∣ x - y ∣ / δ^{2}$ there, by the reverse triangle inequality (Open ball, closed ball and sphere in a metric space, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, The finite and reverse triangle inequalities for a norm; and for $n \geq 1$ every norm $N$ on $R^{n}$ satisfies $N (x) \leq C ∥ x ∥_{1}$ and is Lipschitz, hence continuous, for $d_{2}$ , Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form, A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions).

[F5]

Closure is the smallest closed superset: if $A \subseteq F$ and $F$ is closed then $\overline{A} \subseteq F$ ; closed balls and spheres in $R^{3}$ are compact, hence closed (The closure of a nonempty $A$ is ${x : d (x, A) = 0}$ , equals $A$ together with its limit points, and is the smallest closed superset, For $n \geq 1$ , every Euclidean closed ball and every Euclidean sphere of positive radius is compact).

[F6]

The boundary of the open set $U$ is $\partial U = \overline{U} ∖ U$ ; for an open set the interior is the set itself (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space).

[F7]

Unwinding hypothesis (iii): for every $ε > 0$ there is $δ > 0$ with $∣ w (x) ∣ \leq ε / ∣ x - p ∣$ for all $x$ in $\overline{H} ∖ {p}$ with $0 < ∣ x - p ∣ < δ$ (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form).

[F8]

Hypothesis (iv) says exactly that for every $ε > 0$ there is $ρ > 0$ with $∣ w (x) ∣ \leq ε$ for all $x \in H$ with $∣ x ∣ > ρ$ (Open ball, closed ball and sphere in a metric space).

[F9]

Countable Choice holds in the ambient measure conventions inherited from the kernel supplier; the argument below is pointwise and uses no choice principle (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct

1.1givenF3F7F8

Fix $y \in H ∖ {p}$ and $η > 0$ . By [F8] there is $ρ > 0$ with $∣ w ∣ \leq η$ on $H \cap {∣ x ∣ > ρ}$ ; put $R : = \max {ρ, 2 a, ∣ y ∣} + 1$ , so that $R > ∣ p ∣ + a$ , $R > ∣ y ∣$ and $∣ w ∣ \leq η$ on $H \cap {∣ x ∣ \geq R}$ . By [F7] there is $δ_{0} > 0$ with $∣ w (x) ∣ \leq η / ∣ x - p ∣$ whenever $0 < ∣ x - p ∣ < δ_{0}$ ; put $δ : = \frac{1}{2} \min {δ_{0}, a / 2, ∣ y - p ∣, R - ∣ p ∣}$ , so $0 < δ < a / 2$ , $δ < ∣ y - p ∣$ , $δ < R - ∣ p ∣$ and $δ < δ_{0}$ . Define the open set $U : = H \cap B_{R} (0) \cap {x : ∣ x - p ∣ > δ}$ , the barrier $b (x) : = ∣ x - p ∣^{- 1}$ , and $v_{\pm} : = \pm w - η (1 + b)$ on $U$ .

2.1F4F5F8step 1.1

$U$ is bounded, nonempty and open, and $y \in U$ ; explicitly, $R > ∣ y ∣$ and $δ < ∣ y - p ∣$ put $y$ in $U$ . The closure satisfies $\overline{U} \subseteq \overline{H} \cap \overline{B_{R} (0)} \cap {x : ∣ x - p ∣ \geq δ}$ : each of $\overline{H}$ , $\overline{B_{R} (0)}$ and ${x : ∣ x - p ∣ \geq δ}$ is closed (the last is the complement of the open ball $B_{δ} (p)$ ) and contains $U$ , so [F5] applies factor by factor. In particular $∣ x - p ∣ \geq δ > 0$ on $\overline{U}$ , so $p \notin \overline{U}$ and $\overline{U} \subseteq \overline{H} ∖ {p}$ .

3.1F2F3F4step 1.1step 2.1

Each $v_{\pm}$ lies in $C^{2} (U) \cap C (\overline{U})$ and satisfies $Δ v_{\pm} = 0$ on $U$ . Indeed $U \subseteq H ∖ {p}$ by construction, where $w$ is $C^{2}$ and $Δ w = 0$ , while $b = ω_{2} Φ (\cdot - p)$ is $C^{\infty}$ and harmonic off $p$ [F3]; constants are $C^{\infty}$ ; $Δ$ is linear and annihilates constants [F2], so $Δ v_{\pm} = \pm Δ w - η (0 + Δ b) = 0$ . Continuity on $\overline{U}$ holds because $w$ is continuous there by (i) and step 2.1, and $b$ is continuous on $\overline{U}$ by [F3] and [F4], the bound $∣ x - p ∣ \geq δ$ giving $∣ b (x) - b (y) ∣ \leq ∣ x - y ∣ / δ^{2}$ ; sums and scalar multiples of continuous functions are continuous [F4].

3.2F6givenstep 1.1step 2.1

Each $v_{\pm}$ is nonpositive on $\partial U$ . Let $x \in \partial U = \overline{U} ∖ U$ [F6]. Since $x \in \overline{U}$ and $x \notin U$ , at least one of $x_{3} = 0$ , $∣ x ∣ = R$ , $∣ x - p ∣ = δ$ holds, by the description of $\overline{U}$ in step 2.1 and the definition of $U$ . If $x_{3} = 0$ then $w (x) = 0$ by (ii), so $v_{\pm} (x) = - η (1 + b (x)) < 0$ . Otherwise $x_{3} > 0$ , and since at least one of the three conditions holds, $∣ x ∣ = R$ or $∣ x - p ∣ = δ$ (or both); if $∣ x ∣ = R$ then $∣ w (x) ∣ \leq η$ by the choice of $R$ in step 1.1, so $v_{\pm} (x) \leq η - η (1 + b (x)) = - η b (x) < 0$ , and if $∣ x - p ∣ = δ$ then $∣ w (x) ∣ \leq η / δ = η / ∣ x - p ∣$ by the choice of $δ$ in step 1.1 (and $x \in \overline{H} ∖ {p}$ by step 2.1), so $v_{\pm} (x) \leq η b (x) - η (1 + b (x)) = - η < 0$ .

4.1F1step 3.1step 3.2

The weak maximum principle applies to each $v_{\pm}$ on the bounded nonempty open set $U$ [step 2.1, step 3.1] and gives $\max_{\overline{U}} v_{\pm} = \max_{\partial U} v_{\pm} \leq 0$ by step 3.2, so $v_{\pm} \leq 0$ on $\overline{U}$ . In particular at $y \in U \subseteq \overline{U}$ , $\pm w (y) \leq η (1 + ∣ y - p ∣^{- 1})$ .

5.1givenF9step 1.1step 4.1∎

Since $η > 0$ was arbitrary in step 1.1 and the bound of step 4.1 holds for every $η > 0$ , the real number $t : = ∣ w (y) ∣$ satisfies $t \leq η (1 + ∣ y - p ∣^{- 1})$ for every $η > 0$ ; if $t > 0$ then $η : = t / (2 (1 + ∣ y - p ∣^{- 1})) > 0$ gives $t \leq t / 2 < t$ , a contradiction, so $t = 0$ , that is $w (y) = 0$ . As $y \in H ∖ {p}$ was arbitrary, $w = 0$ on $H ∖ {p}$ . This proves uniqueness in the stated sub-Coulomb class; no removable-singularity theorem, no boundedness or growth assumption beyond (iii)-(iv), and no boundary regularity beyond the flat trace (ii) was used, and the only ambient choice convention is the one inherited from the kernel interfaces [F9].

Uniqueness for harmonic functions on a punctured half-space with zero trace, decaying at the pole and at infinity

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources