Thomae's (Popcorn) Function

Stream: general

[Ender Doe]

Hello All. Recently I finished proving the main results for Thomae's (Popcorn) function, thomaes_continous_at_irrationals : ∀ x, irrational x → continuous_at thomaes_function x.

The lean file is pretty messy and has a lot of bloat, and I am working on cleaning up the code. Wanted to make this topic in case anyone is interested in this result or is also attempting to formalize. Perhaps in the future the repo might be a candidate for mathlib, but needs significantly more work.

As far as I am aware this is the first computer proof of Thomae's function? Would be curious if wrong.

https://github.com/FrickHazard/thomaes-function

[Eric Rodriguez]

cool stuff! from some quick glancing, a tactic you may like a lot is assumption_mod_cast