Skip to content

Latest commit

 

History

History
16 lines (11 loc) · 520 Bytes

README.md

File metadata and controls

16 lines (11 loc) · 520 Bytes

Thomaes (Popcorn) function proofs in Lean.

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

Thomae_function_(0,1) svg

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