For a harmonic function and Brownian motion stopped before leaving its domain, Itô formula gives . The drift vanishes. On a compact subdomain, the stopped process is a bounded martingale. Optional stopping theorem at an almost-surely finite exit time therefore gives the boundary mean formula. At the centre of a disk, rotational invariance of planar Brownian motion makes the exit law uniform on the boundary circle. This proves the mean value property for harmonic functions probabilistically.
Let , and suppose has a local maximum at . Choose such that the closed disk lies in and throughout it. Start planar Brownian motion at , and for let be its first exit from .
By part (a) and Itô formula, is a local martingale; boundedness of on the compact disk makes it a true bounded martingale. The exit time is finite almost surely. One direct check applies the same formula to , giving . Thus .
The optional stopping theorem, first at and then by bounded convergence, gives
The exit point is uniformly distributed on the circle: rotational invariance of planar Brownian motion about its starting point makes its exit law rotation invariant, and normalized arc length is the unique rotation-invariant probability measure on a circle. Since every boundary value is at most , equality of the mean forces every boundary value to equal ; continuity rules out a strict deficit at any boundary point. This holds for every , so is constant on the entire disk.
The Cauchy-Riemann equations then give both partial derivatives of equal to zero there. Thus is constant on that disk. The identity theorem for holomorphic functions propagates this constant to the connected component of in . Applying the same Brownian argument to proves the assertion for the imaginary part as well:
If is connected, this is constancy on all of . For a disconnected open set the printed global wording needs this qualification: a function taking different constants on two disjoint disks is holomorphic and has local maxima on each disk while not being globally constant.
Put . The hitting times are finite almost surely by recurrence of planar Brownian motion, and increase with . At , the position is . By the Strong Markov property, Brownian scaling, and rotational invariance of planar Brownian motion, the future process
is a standard planar Brownian motion started at , independent of . The random rotation does not change its conditional law, since that law is rotationally invariant.
The first time this rescaled process reaches radius corresponds to the original time . Its continuous argument starts at zero and equals the increment of the original winding angle. Hence
For any ordered finite collection of levels, apply this assertion successively. Earlier winding values are measurable at the current hitting time, so all increments are independent and their laws depend only on the level differences. This proves the Lévy process property of winding at logarithmic radial passage levels.
One can also verify stochastic continuity and identify this process. The logarithmic-radius and argument martingales have the common clock
The same Cauchy-Riemann equations calculation as in part (a), applied locally to the logarithm and joined along the continuous argument, gives independent Brownian motions such that and . This clock diverges: if it had a finite limit, convergence of martingales with finite total quadratic variation would make converge to a finite value, forcing the clock integral itself to diverge.
Thus, with , we have . The Brownian first-passage Laplace transform is . It follows either from the Exponential martingale for Brownian motion stopped at , or from the one-dimensional exit equation. Conditioning on the independent process gives
So this is a symmetric Cauchy process, with level parameter . The formula implies stochastic continuity at zero and, by stationary increments, everywhere. Under the usual definition requiring càdlàg paths, use the right-continuous passage clock . It agrees with for each fixed level almost surely, and is the càdlàg modification. This distinction concerns simultaneous passage levels and does not alter any increment law.
Scale the disk to the unit disc, so that the starting point is . Use the Möbius transformation
which maps the disk onto itself, sends to , and sends to . By conformal invariance of planar Brownian motion, the exit image is the circular exit of a Brownian motion starting at . Rotational invariance of planar Brownian motion makes that exit uniform in angle.
The endpoints of the right semicircle satisfy
Its image is the arc through between these points, of angular length . Thus the Möbius calculation of circular Brownian exit gives
Since and partition the exit almost surely, part (b) yields
The last equality uses , so the double-angle tangent identity uses the stated principal branch. As a check, the boundary angle derivative of is ; integrating this circular exit density over the right semicircle gives exactly the integral supplied in the question.