Thomaes (Popcorn) function proofs in Lean.

Description of function here https://en.wikipedia.org/wiki/Thomae%27s_function.

DONE

• Proof of periodicity
• Proof of Continuity at irrationals
• Proof of discontinuity at rationals.

TODO

• Proof of nowhere differentiable.
• Proof of Riemann integrable and eq to 0 for any interval
• Proof of rational numbers are local maximums