Brownian motion w.p. 1 is nowhere differentiable in (0,1)

Stream: new members

[Lars Ericson]

Just throwing this out there as a long-term goal to prove in Lean. It's a one-and-a-half page proof so it seems like a pretty well scoped goal, but over my head at the moment: https://math.uchicago.edu/~may/VIGRE/VIGRE2007/REUPapers/FINALAPP/Olson.pdf

[Bryan Gin-ge Chen]

Maybe an easier task: construct the Weierstrass function and prove that it is eveywhere continuous and nowhere differentiable.

[Heather Macbeth]

The Takagi function would probably be easier than the Weierstrass one.