Compact convergence of locally bounded harmonic functions (source code)

= Compact convergence of locally bounded harmonic functions

A locally uniformly bounded sequence of <harmonic functions> with a pointwise limit converges uniformly on compact subsets, and its limit is harmonic. A radial <mollifier> of fixed local radius reproduces each harmonic function by the <mean value property for harmonic functions>. Differentiating that convolution gives uniform interior gradient bounds, hence equicontinuity. A finite covering of a compact set converts pointwise convergence to uniform convergence. Passing to the limit in the radial convolution identity proves smoothness; passing to the limit against the Laplacian of each <test function> proves harmonicity.