Suppose we define the local time $L_0(t, \omega)$ of the standard Brownian motion $B(s, \omega): [0,t] \times \Omega \rightarrow \mathbb{R}$ by
$$ L_0(t, \omega) = \lim_{\epsilon \rightarrow 0} \frac{1}{2 \epsilon} m(\{ s \in [0,t], B(s, \omega) \in (-\epsilon, \epsilon)\}) $$
where $m$ is the Lebesgue measure.
This looks like the derivative of the push-forward measure (by the sample path $B(s;\omega): [0,t] \rightarrow \mathbb{R}$) with respect to the Lebesgue measure at $0$. So the existence of $L_0(t, \omega)$ just follows from apply standard real analysis results $\omega$-by-$\omega$, correct?
(I've seen arguments that use Ito's lemma to establish existence by smoothing out the absolute value function at $0$. I am wondering if this is necessary, if one is only interested in establishing existence.)