> [!theorem]
>
> Let $\bracs{B_t: t \ge 0}$ be the standard [[Brownian Motion]] on $(\Omega, \cf, \bracs{\cf_t}, \bp)$, where $\bracs{\cf_t}$ is the natural filtration. Let $F: [0, \infty) \to \real$ such that $F(\cdot, x) \in C^1$, $F(t, \cdot) \in C^2$, and $F, \partial_t F, \partial_x F, \partial_{xx} F$ are all bounded. Then
> $
> \begin{align*}
> F(t, B_t) - F(0, 0) &= \int_0^t \partial_t F(s, B_s)ds + \int_0^t \partial_x F(s, B_s)dB_s \\
> &+ \frac{1}{2}\int_0^t\partial_{xx}F(s, B_s)ds
> \end{align*}
> $
> where the second integral is an [[Itô's Integral]]. Alternatively,
> $
> dF(t, B_t) = \partial_t F(t, B_t)dt + \partial_x F(t, B_t)dB_t + \frac{1}{2}\partial_{xx}F(t, B_t)dt
> $
> *Proof*. Suppose that $F \in C_c^\infty$. Let $C_F = \norm{F}_u + \norm{DF}_u + \norm{D^2F}_u + \norm{D^3F}_u$.
>
> Given $N \in \nat$ and $t \ge 0$, let $\tau_0^N = 0$, and for $m \ge 1$, define
> $
> \tau_m^N = t \wedge (\tau_{m - 1}^N + 2^{-N}) \wedge \inf\bracs{s \ge \tau_{m - 1}^N: \abs{B_s - B_{\tau_{m - 1}^N}} \ge 2^{-N}}
> $
> then $\tau_m^N$ are all [[Stopping Time|stopping times]] with respect to $\bracs{\cf_t}$.
>
> For each $\omega \in \Omega$, $B(\omega)$ is uniformly continuous on $[0, t]$. There exists $\delta_\omega \in (0, 2^{-N})$ such that for any $s, s' \in [0, t]$ with $\abs{s - s'} < \delta_\omega$, $\abs{B_s - B_{s'}}(\omega) < 2^{-n}$. Thus $\tau_m^N(\omega) - \tau_{m - 1}^{N}(\omega) \ge \delta_\omega$ for all $m \in \nat$. Therefore, for any fixed $\omega \in \Omega$, $\tau_m^N(\omega) = t$ for sufficiently large $m$.
>
> This allow partitioning
> $
> F(t, B_t) - F(0, 0) = \sum_{m = 1}^\infty \braks{F(\tau_m^N, B_{\tau_m^N}) - F(\tau_{m-1}^N, B_{\tau_{m - 1}^N})}
> $
> Over a Taylor expansion,
> $
> \begin{align*}
> &F(\tau_m^N, B_{\tau_m^N}) - F(\tau_{m-1}^N, B_{\tau_{m - 1}^N}) \\
> &= F(\tau_m^N, B_{\tau_m^N}) - F(\tau_{m-1}^N, B_{\tau_{m}^N}) + F(\tau_{m-1}^N, B_{\tau_{m}^N}) - F(\tau_{m-1}^N, B_{\tau_{m - 1}^N}) \\
> &= \int_{\tau_{m - 1}^N}^{\tau_m^N}\partial_s F(s, B_{\tau_m^N})ds + \partial_xF(\tau_{m - 1}^N, B_{\tau_{m-1}^N})(B_{\tau_{m}^N} - B_{\tau_{m - 1}^N}) \\
> &+ \frac{1}{2}\partial_{xx}F(\tau_{m - 1}^N, B_{\tau_{m-1}^N})(B_{\tau_{m}^N} - B_{\tau_{m - 1}^N})^2 + R_m
> \end{align*}
> $
> and denote $\Delta B_m^{N} = B_{\tau_m^N} - B_{\tau_{m - 1}^N}$. By regrouping,
> $
> \begin{align*}
> F(t, B_t) - F(0, 0) &= \sum_{m = 1}^\infty \int_{\tau_{m - 1}^N}^{\tau_m^N}\partial_s F(s, B_{\tau_m^N})ds + \sum_{m = 1}^\infty \partial_xF(\tau_{m - 1}^N, B_{\tau_{m-1}^N})(\Delta B_m^{N})\\
> &+ \sum_{m = 1}^\infty \partial_{xx}F(\tau_{m - 1}^N, B_{\tau_{m-1}^N})(\Delta B_m^{N})^2 + \sum_{m = 1}^\infty R_m
> \end{align*}
> $
> The second sum coincides with a Riemann-Stieltjes sum, so sending $N \to \infty$,
> $
> \sum_{m = 1}^\infty \partial_x F(\tau_{m - 1}^N, B_{\tau_{m - 1}^N})(\Delta B_m^N) \to \int_0^t\partial_x F(s, B_s)dB_s
> $
> in $L^2$. On the other hand, for every $m \ge 1$ and $s \in [\tau_{m - 1}, \tau_m]$,
> $
> \abs{\partial_s F(s, B_s) - \partial_s F(s, B_{\tau_m})} \le C_F\abs{B_s - B_{\tau_m}} \le C_F2^{-N}
> $
> Therefore
> $
> \begin{align*}
> &\abs{\sum_{m = 1}^\infty \int_{\tau_{m - 1}^N}^{\tau_m^N}\partial_s F(s, B_{\tau_m^N})ds - \int_0^t \partial_sF(s, B_s)ds} \\
> &\le \abs{\sum_{m = 1}^\infty \int_{\tau_{m - 1}^N}^{\tau_m^N}\partial_s F(s, B_{\tau_m^N})ds - \sum_{m = 1}^\infty \int_{\tau_{m - 1}^N}^{\tau_m^N}\partial_sF(s, B_s)ds} \\
> &\le \sum_{m = 1}^\infty \int_{\tau_{m - 1}^N}^{\tau_m^N}\abs{\partial_s F(s, B_s) - \partial_s F(s, B_{\tau_m})} \\
> &\le \sum_{m = 1}^\infty \int_{\tau_{m - 1}^N}^{\tau_m^N}C_F2^{-N} \le 2^{-N}C_Ft \to 0 \quad (N \to \infty)
> \end{align*}
> $
> For the remainders,
> $
> \abs{R_m} \le C_F (\Delta B_m^N)^3 \le 2^{-N}C_F (\Delta B_m^N)^2
> $
> so
> $
> \ev\braks{\abs{\sum_{m = 1}^\infty R_m}^2} \le 2^{-2N}C_F^2 \ev\braks{\sum_{m = 1}^\infty (\Delta B_m^N)^2} \le 2^{-2N}C_F^2 t
> $
> which goes to $0$ in $L^2$.
>
> For the third term, if $s \in [\tau_{m - 1}, \tau_m]$, then
> $
> \abs{\partial_{xx}F(\tau_{m - 1}^N, B_{\tau_{m - 1}^N}) - \partial_{xx}F(\tau_{m - 1}^N, B_s)} \le 2^{-N}C_F
> $
> so
> $
> \begin{align*}
> &\abs{\sum_{m = 1}^\infty \partial_{xx}F(\tau_{m - 1}^N, B_{\tau_{m-1}^N})(\Delta B_m^{N})^2 - \int_0^t\partial_{xx}F(s, B_s)ds} \\
> &\le \abs{\sum_{m = 1}^\infty \partial_{xx}F(\tau_{m - 1}^N, B_{m - 1}^N)\braks{(\Delta B_m^N)^2 - (\tau_m - \tau_{m - 1})}} \\
> &+ \abs{\sum_{m = 1}^\infty \int_{\tau_{m - 1}^N}^{\tau_{m}^{N}}\braks{\partial_{xx}F(\tau_{m - 1}^N, B_{\tau_{m - 1^N}}) - \partial_{xx}F(s, B_s)}ds}
> \end{align*}
> $
> where the second term goes to $0$ as $N \to \infty$. For the first term,
> $
> \begin{align*}
> &\abs{\sum_{m = 1}^\infty \partial_{xx}F(\tau_{m - 1}^N, B_{m - 1}^N)\braks{(\Delta B_m^N)^2 - (\tau_m - \tau_{m - 1})}} \\
> &\le C_F \abs{\sum_{m = 1}^\infty \braks{(\Delta B_m^N)^2 - (\tau_m - \tau_{m - 1})}} \to 0
> \end{align*}
> $
> in $L^2$ as $n \to \infty$.
If $\varphi \in \Phi^2$ and $F \in C_c^\infty([0, \infty) \times \real)$,
$
\begin{align*}
F(t, \mathcal I(\varphi)_t) - F(0, 0) &= \int_0^t \partial_s F(s, \mathcal I(\varphi)_s)ds + \int_0^t \partial_sF(s, \mathcal I(\varphi)_s)\varphi_s dB_s \\
&+ \frac{1}{2}\int_0^t \partial_{xx}F(s, \mathcal I(\varphi)_s)\varphi_s^2 dt
\end{align*}
$