Stream: new members
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: May 16 2021 at 05:21 UTC