Chebyshev Functions

Stream: Is there code for X?

[Roman Kvasnytskyi]

I would like to contribute to Number Theory by working on formalizing Chebyshev Functions. As I can see, defining them is feasible. Is there any ongoing work on it, or maybe you have any suggestions or words of caution against this idea?

[Kim Morrison]

Do you mean docs#Polynomial.Chebyshev.T and the other declarations in that file?

[Weiyi Wang]

Or https://en.m.wikipedia.org/wiki/Chebyshev_function ? Looks like something PNT+ might have

[Weiyi Wang]

Like this? https://alexkontorovich.github.io/PrimeNumberTheoremAnd/docs/PrimeNumberTheoremAnd/MediumPNT.html#ChebyshevPsi

[Roman Kvasnytskyi]

Yes, I meant Chebyshev functions that go around PNT theorem. Alex Kontorovich PNT repo have exactly what I need, thanks.