reverse mathematics strength of "Lipschitz functions are somewhere differentiable" What is the reverse mathematics strength of

"For all Lipschitz functions $\; f : \mathbb{R} \to \mathbb{R} \;$, $\;$ there exists a real number $x$ such that $f$ is differentiable at $x$." ?

(defined using epsilon-delta, so not requiring that there exist a function witnessing the convergence)
Since Lipschitz functions are differentiable almost everywhere,

I would guess the answer is "is equivalent to WWKL$_0$ (over RCA$_0$)".
 A: (Update: I made my answer clearer and also fixed the references and added more.)
Your theorem should be true in every $\omega$-model of $\mathsf{RCA}_0$ as follows. The following paper


*

*Brattka, Miller and Nies. Randomness and Differentiability.  Submitted.  (preprint)


proves that every computable function on $[0,1]$ that is Lipschitz is differentiable on all computable randoms.  Further, from this proof, I believe you can extract a single computable martingale $M$ such that if $x$ is a point of differentiability of $f$, then $M$ does not succeed on $x$.  Unlike ML randomness---which corresponds to $\mathsf{WWKL}_0$---with a test for computable randomness, i.e. the computable martingale $M$, you can compute a real $y$ such that $M$ doesn't succeed on $y$.

Hence there is (I believe) a real $y$
  computable from the function $f$ for which $f$ is
  differentiable at $x$.
Hence your theorem holds in every $\omega$-model of $\mathsf{RCA}_0$.
This implies that your theorem
  is true in $\mathsf{RCA}_0$ or $\mathsf{RCA}_0$ plus some first order principle.

I should mention, I learned of this trick from Steve Simpson (in the case of Schnorr randomness). 
Of course to see if it is provable in ${RCA}_0$, you should check that level of induction/collection used. A recent paper with Jeremy Avigad and Ed Dean,


*

*Avigad, Dean and Rute. Algorithmic
Randomness, reverse mathematics, and
the dominated convergence theorem. Submitted (preprint)


gives an example where the dominated convergence thereom, in a sense, corresponds to $2$-randomness, but the reverse math strength of the dominated convergence thereom was a bit higher, since $\Sigma^0_2$ collection was needed.
(You do not not seem to need this, but...) even though you know a point $x$ such that $f$ is differentiable, that doesn't mean you know what the derviative is at that point. Actually, you can't even compute the derivative $f'$ in the $L^1$ norm.
There are more published and unpublished works related to the diffentiability of computable functions.  One good summary of the recent work in this area is the Logic Blog on Andre Nies's website. Another is this talk by Nies.
There are also three results in preparation that may be of value.  I proved, as did Pathak, Rojas and Simpson independently, that the Lebesgue differentiation theorem holds on Schnorr randoms.  In particular this implies that a more restrictive notion of computable Lipschitz function is differentiable on Schnorr randoms (see Nies' talk mentioned above). Freer, Kjos-Hanssen and Nies, have a paper in preparation about Lipschitz functions and differentiability, which in a sense, "reverses" the above results. (Again, this is mentioned in the talk by Nies.)
A: Here it is, the newest version
http://dl.dropbox.com/u/370127/papers/randomnessanalysisjuly_2011.pdf
What jason says is right, even for nondecreasing functions. It is in our paper, Subection 5.1
Hence there is (I believe) a real $y$ computable from the function $f$ for which $f$ is differentiable at $x$.
Hence your theorem holds in every $\omega$-model of RCA0.
This implies that your theorem is true in RCA0 or RCA0 plus some first order principle.
Not sure what these fo principles do, I guess it's standard stuff?
