Theorem 4.4.52F74CBABB2A6

Proof. The convex function $|x-a|$ is subharmonic by Jensen on harmonic coordinate functions, so lies in the lower class for $m$. Thus $H_ m\ge |x-a|>0$. Let $w$ be a weak local barrier, and choose a small sphere of radius $r$ centered at $a$ within its domain. Put $M=\max _{\partial D}|z-a|$. Choose compact $F\subset D\cap \partial B(a,r)$ whose complement in that open spherical set has normalized area less than $r/M$; if the open set is empty no $F$ is needed and comparison directly gives $H_ m\le r$ inside. Otherwise $k=\inf _ Fw>0$ (if $F$ is empty choose it nonempty by taking a smaller error). Let $b$ be the ball Poisson integral of boundary data $M$ on $(D\cap \partial B)\setminus F$ and zero elsewhere. It is nonnegative, continuous near the center, with $b(a)<r$. For every lower competitor $v$ for $m$, bounded comparison on $D\cap B$ gives

On $F$ the $w$ term dominates the bound $v\le M$; on the remaining open sphere the Poisson limit is $M$; on the original boundary $v$ has upper limit at most $m\le r$. These verify every boundary piece. Taking the supremum and then approaching $a$ gives $\limsup H_ m\le 2r$. Let $r\to 0$. The global barrier and its positive-away-from-$a$ lower bound now follow from $H_ m\ge |x-a|$. For bounded-above data with local limsup $L$, the function $L+\varepsilon +cH_ m$ belongs to the upper class when $c$ is large enough to control the data outside a small neighborhood. Its limit at $a$ is $L+\varepsilon $. The case $L=-\infty $ is handled with any finite upper target instead. Negation gives the lower inequality. Conversely, regularity applied to continuous $m$ makes $H_ m$ a weak barrier. $\square$