Zulip Chat Archive

Stream: new members

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

Lars Ericson (Feb 06 2021 at 18:02):

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 (Feb 06 2021 at 18:16):

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

Heather Macbeth (Feb 06 2021 at 18:31):

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

Last updated: Dec 20 2023 at 11:08 UTC