What is the [reverse mathematics](http://en.wikipedia.org/wiki/Reverse_mathematics) strength of
  

"For all [Lipschitz](http://en.wikipedia.org/wiki/Lipschitz_continuity) 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$)".



reverse mathematics strength of "Lipschitz functions are somewhere differentiable"
(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](http://dl.dropbox.com/u/370127/papers/randomnessanalysisjuly_2011.pdf))


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](http://arxiv.org/abs/1106.0775))


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](http://www.cs.auckland.ac.nz/~nies/). Another is this [talk](http://dl.dropbox.com/u/370127/talks/RandomnessComputableAnalysisNies.pdf) 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.)


