Removable singularity for a bounded harmonic function (source code)

= Removable singularity for a bounded harmonic function

A <harmonic function> on a punctured ball that is bounded near the missing point extends uniquely to a harmonic function on the whole ball. The extension can be defined by the <mean value property for harmonic functions>; interior estimates then give smoothness across the point.