TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Hopf boundary point lemma for the laplacian

Statement

Let $n \geq 2$ , let $Ω \subseteq R^{n}$ be open, and suppose $B_{R} (a) \subset Ω$ is an interior tangent ball at $p \in \partial Ω$ . Let $u \in C^{2} (Ω)$ be subharmonic, with a continuous extension to ${\overline{B}}_{R} (a)$ , such that $u (x) < M$ for every $x \in Ω$ and $u (p) = M$ . If the finite derivative $\partial_{ν} u (p)$ exists for $ν = (p - a) / R$ , then $\partial_{ν} u (p) > 0$ .

Facts & Assumptions

Given: The objects and hypotheses in the statement.

[F1]

The exponential annulus barrier is subharmonic, has inner value one and outer value zero, and has strictly negative outward derivative. (Interior sphere barrier for the laplacian).

[F2]

The weak maximum principle controls a subharmonic function on a bounded nonempty open set by its boundary values when it is continuous on the closure. (Weak maximum principle for the laplacian).

[F3]

Closed bounded Euclidean sets are compact (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

[F4]

A continuous real function on a nonempty compact metric space attains a minimum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[F5]

A connected space has no separation into two nonempty disjoint open subsets (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets).

Proof

technique · direct

1.1F1given

On the compact inner sphere, continuity and strict inequality give $ε = M - \max_{∣ x - a ∣ = R / 2} u (x) > 0$ . Take the exponential barrier $v$ , equal to one on that sphere and zero on the outer sphere.

1.2F5givenalgebra

Here is the additional Hopf route to the strong subharmonic principle. Suppose $U$ is a domain and $f \in C^{2} (U)$ satisfies $Δ f \geq 0$ and $f \leq M$ in $U$ , and $E = {f = M}$ is nonempty but not all of $U$ . It is relatively closed. Its complement $G$ is nonempty open, and some $y \in E$ is a relative boundary point of $G$ ; otherwise $E$ and $G$ would separate $U$ . Choose $d > 0$ with ${\overline{B}}_{d} (y) \subset U$ and $x \in G$ with $∣ x - y ∣ < d / 4$ .

2.1F1F2step 1.1

Continuity from inside the tangent ball gives $u \leq M$ on its entire outer sphere. On the annulus, $w = u + ε v - M$ is subharmonic and continuous on the closure, and its values are at most zero on both boundary spheres. The weak maximum principle gives $w \leq 0$ throughout the annulus.

2.2F3F4step 1.2algebra

Set $r = \inf_{z \in E} ∣ x - z ∣$ . Openness of $G$ gives $r > 0$ , and $r \leq ∣ x - y ∣ < d / 4$ . A closest point $q \in E$ exists: minimize distance on the nonempty compact set $E \cap {\overline{B}}_{d / 2} (y)$ ; points of $E$ outside this set have distance from $x$ greater than $d / 4$ , so this also minimizes over all of $E$ . The ball $B_{r} (x)$ lies in $G$ , its closure lies in $U$ , and $q$ is on its sphere.

3.1F1step 2.1algebra

For $0 < t < R / 2$ , $u (p) - u (p - t ν) \geq ε v (p - t ν)$ . Divide by $t > 0$ and pass to the assumed finite limit: $\partial_{ν} u (p) \geq - ε \partial_{ν} v (p) > 0$ .

4.1step 3.1step 2.2algebra∎

Apply the boundary conclusion already proved in step 3.1 to $f$ on $G$ , with this tangent ball and boundary point $q$ . It gives a positive outward derivative. But $q \in U$ is an interior maximum of the differentiable function $f$ , so all its first derivatives are zero and this directional derivative is zero. Therefore $E = U$ and $f$ is constant. This alternative uses no mean inequality.

Depends on

Used by

Hopf conclusion needs a strict nonconstant extremum Counterexample
Hopf lemma needs a boundary geometry hypothesis Counterexample
Harmonic function attaining only boundary extrema Example
Maximum principles need domain and boundary hypotheses Remark

Dependency tree · two levels

52 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

Hunter, Notes on Partial Differential Equations (standard reference, not scraped)