Theorem 4.4.128FA95EB71F47

Proof. At finite points the minimum-set argument is the checked Euclidean one. If the minimum is attained at infinity, each large sphere mean is at least the minimum and at most the value there. Lower semicontinuity and positivity of the surface measure of open patches force equality at every point of each such sphere. Thus the minimum set contains an exterior neighborhood and is open and closed. For a proper open set each component has a nonempty boundary in the connected compact ambient space. Extend by boundary liminf; compactness forces a negative minimum to be attained inside if any negative value exists. The strong minimum principle would make the component a negative constant, contradicting its nonnegative boundary limits. For the entire compact space a minimum is attained and the function is constant; one cannot infer a nonnegative constant from an empty boundary.

For algebraic operations use the ordinary local result and the linear sphere inequalities at infinity; nontriviality follows from finite almost everywhere values on each Euclidean component. For exterior lowering, increasing continuous minorants of the lsc sphere data and the positive exterior Poisson kernel give a harmonic minorant bounded above by $u$ via compactified comparison. Finite interior values exclude an infinite limit. The same boundary-liminf/pasting proof as for interior lowering makes the replacement superharmonic at finite points. Near infinity it is the exterior harmonic solution with constant large-sphere means equal to its value there. For every other allowed sphere center, the finite-point superharmonic mean is concave as a function of $r^{2-d}$ (or $-\log r$ in the plane), and is constant at that value for all sufficiently large radii, by the zero-flux argument above. Concavity bounds its earlier means by the same value, giving the required inequality at infinity. Directed harmonic limits reduce to the Euclidean result away from infinity and the positive exterior kernel on a fixed sphere near infinity; directed monotone integration identifies the value and harmonicity there. The saturated-family proof then applies in both kinds of neighborhoods, exactly as for finite balls, with nonemptiness explicitly required.

For $d=2$, $\log |x-a|$ on an exterior neighborhood, with value infinity at infinity, is a superharmonic pole function there. For $d\ge 3$, concentric sphere means of a superharmonic function on an exterior are finite and concave functions of $t=r^{2-d}$. A supporting affine upper bound at an interior $t$ bounds them above as $t\downarrow 0$. If the value at infinity were infinite, lsc would instead force all sufficiently distant sphere means to tend to infinity. This contradiction proves nonpolarity. $\square$