A Constructive Brownian Limit Theorem

In this paper, we present and prove a boundary limit theorem for Brownian motions for the Hardy space $\mathbf{h}^{p}$ of harmonic functions on the unit ball in $R^m$, where $p\geq1$ and $m\geq2$ are arbitrary. Our proof is constructive in the sense of [Bishop and Bridges 1985, Chan 2021, Chan 2022]. Roughly speaking, a mathematical proof is constructive if it can be compiled into some computer code with the guarantee of exit in a finite number of steps on execution. A constructive proof of said boundary limit theorem is contained in [Durret 1984] for the case of $p>1$. In this article, we give a constructive proof for $p=1$, which then implies, via the Lyapunov's inequality, a constructive proof for the general case $p\geq1$. We conjecture that the result can be used to give a constructive proof of the nontangential limit theorem for Hardy spaces $\mathbf{h}^{p}$ with $p\geq1$. We note that, ca 1970, R. Getoor gave a talk on the Brownian limit theorem at the University of Washington. We believe that the proof he presented is constructive only for the case $p>1$ and not for the case $p=1$. We are however unable to find a reference for his proof.