The regularized Perron envelope is harmonic

By [L1], the family $\mathcal{P}(\phi ,\mathrm{\Omega })$ is locally bounded above. Applying [L5] to that family shows that $H_{\phi }$ is subharmonic on $\mathrm{\Omega }$.

Fix $z_0\in \mathrm{\Omega }$ and choose a closed disc $\bar{D}⋐\mathrm{\Omega }$ centered at $z_0$. By the definition of upper-semicontinuous regularization, choose points $z_n\to z_0$ with $U_{\phi }(z_n)>H_{\phi }(z_0)-1\mathrm{/}n$. For each $n$, choose $v_n\in \mathcal{P}(\phi ,\mathrm{\Omega })$ with $v_n(z_n)>U_{\phi }(z_n)-1\mathrm{/}n$.

Put $w_n=\max (v_1,\dots ,v_n)$. By [L3], each $w_n$ lies in the Perron family, and $w_n(z_n)>H_{\phi }(z_0)-1\mathrm{/}n$. Let $h_n=P_D{w}_n$. By [L2], each $h_n$ is harmonic on $D$, belongs to the Perron family, majorizes $w_n$, and the sequence $(h_n)$ is increasing because the sequence $(w_n)$ is increasing. Step [L1] also gives $h_n\le M$ on $D$.

The sequence $(h_n)$ is increasing and bounded above at every point by $M$, so [L4] yields a harmonic limit $h$ on $D$. Since each $h_n$ belongs to the Perron family, one has $h_n\le U_{\phi }\le H_{\phi }$, hence $h\le H_{\phi }$ on $D$. On the other hand, [step 3.1, L4] $H_{\phi }(z_0)-\frac{1}{n}<h_n(z_n)\le h(z_n)\le H_{\phi }(z_n)\mathrm{.}$ Letting $n\to \mathrm{\infty }$ and using continuity of $h$ and upper semicontinuity of $H_{\phi }$ gives $h(z_0)=H_{\phi }(z_0)$.

The function $H_{\phi }-h$ is subharmonic on $D$: both $h$ and $-h$ are harmonic and therefore subharmonic, and [L3] handles sums with positive coefficients. Step 4.1 shows $H_{\phi }-h\le 0$ on $D$ and vanishes at the interior point $z_0$, so [L6] forces $H_{\phi }-h$ to be constant $0$ on $D$. Hence $H_{\phi }=h$ on $D$, and therefore $H_{\phi }$ is harmonic near $z_0$. Since $z_0$ was arbitrary, $H_{\phi }$ is harmonic on $\mathrm{\Omega }$.