Properties of Chebyshev polynomials over the reals

Stream: mathlib4

[Yuval Filmus]

I have proved several properties of Chebyshev polynomials over the reals, such as their roots and extreme points, and also one extremal property of the Chebyshev polynomials: they maximize the leading coefficient.
Where should these results be put? In my draft, they comprise two separate files, one proving the easy properties, and one proving the extremal property. There are many other extremal properties of Chebyshev polynomials that could be proved in the future.
Should I create a new directory for these results and future ones?

[Ruben Van de Velde]

How much code is it? Mathlib.RingTheory.Polynomial.Chebyshev doesn't seem to import \R. Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev has some results, but perhaps not the right place

[Johan Commelin]

I would lean towards Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev... but I'm not an expert on this topic.

[Yuval Filmus]

Johan Commelin said:

I would lean towards Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev... but I'm not an expert on this topic.

That's good for the file with easy properties such as roots and extrema.
What about other files proving various extremal properties of Chebyshev polynomials?
I can try golfing them to a reasonable size, but there are quite a few of them...

[Bryan Gin-ge Chen]

It sounds like it might be reasonable to create a new directory Analysis/SpecialFunctions/Trigonometric/Chebyshev and then have files Basic.lean and Extremal.lean (not sure about the name, maybe ExtremalProperties?) in it.

[Eric Vergo]

The to do list in Mathlib.RingTheory.Polynomial.Chebyshev has a litem "Compute zeroes and extrema of Chebyshev polynomials." so that might be the right place.

Can you share the files you are looking to merge? I am also working on results related to Chebyshev polynomials and defined the roots using cosine values. I would love to update this to a proof and will use yours once it's in mathlib.

[Yuval Filmus]

@Eric Vergo
It's in this closed PR: https://github.com/leanprover-community/mathlib4/pull/31011
I'm waiting for the following PR to be approved before reworking the closed one, which will be divided into at least two PRs: https://github.com/leanprover-community/mathlib4/pull/32360
I also worked out the bound on the derivative at 1, but this requires proving several trigonometric identities, so would be a huge mess to add to Mathlib.

[Yuval Filmus]

The file you mention has several TODO's, and it's clear that not all of them can belong to the same file (considering there are entire books written down on extremal properties of Chebyshev polynomials).

[Eric Vergo]

Yuval Filmus said:

The file you mention as several TODO's, and it's clear that not all of them can belong to the same file (considering there are entire books written down on extremal properties of Chebyshev polynomials).

Indeed, there is a huge body of work that should eventually be formalized. For the results you mentioned we are going to need multiple files regardless of whether it goes into .../trigonometry or .../polynomials. I'm leaning towards .../polynomials but don't know enough to feel strongly about it.

[Ruben Van de Velde]

I think that results that apply specifically to the real numbers should not go under ringtheory

[Yuval Filmus]

So Analysis/SpecialFunctions/Trigonometric/Chebyshev.
A file? A directory? Several files?

[Johan Commelin]

@Yuval Filmus A directory sounds good to me.

[Johan Commelin]

What Bryan suggested here: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Properties.20of.20Chebyshev.20polynomials.20over.20the.20reals/near/563488354

[Yuval Filmus]

There is actually a file Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean with some basic formulas.
I could add the basic stuff there.
In that case, where should the extremal results go?

Alternatively, the file can be moved to a directory Chebyshev and renamed Basic.lean, but that is probably less advisable.

[Yuval Filmus]

Another option is to have both Chebyshev.lean and a Chebyshev directory, which also sounds awkward.
My Basic.lean is hundreds of lines (probably less after golfing).

[Yuval Filmus]

Another complication is that Trigonometric/Chebyshev.lean is about both the complex and the real versions.
Some of my results make sense in both cases (zeroes), but some only make sense for the real polynomials (boundedness, extrema, extremal properties).

[Nick_adfor]

I have also writen some code about Chebyshev polynomial. Maybe some of them can be combined together here.

[Yuval Filmus]

You can take a look at what I wrote: https://github.com/leanprover-community/mathlib4/pull/31011
I'm now golfing the first file (Basic.lean), and also waiting for my previous PR on Chebyshev polynomials to be finally approved.
What have you worked on?

[Snir Broshi]

Yuval Filmus said:

Alternatively, the file can be moved to a directory Chebyshev and renamed Basic.lean, but that is probably less advisable.

AFAIK this is pretty common in Mathlib. You start with a PR that moves Chebyshev.lean to Chebyshev/Basic.lean, then follow it up with a PR that adds back Chebyshev.lean as an almost empty file with a copyright header and a deprecated_module statement, and finally a PR that does whatever you want to do in the folder.

A recent example: #27795 moves AtPrime.lean to AtPrime/Basic.lean, and #27796 adds back AtPrime.lean. The operation is split to 2 PRs to make git see that this is really a move, rather than editing the old file and adding a new file.

[Nick_adfor]

https://github.com/NickAdfor/ChebyshevPolynomial

Some work is here. It can work on v4.16.0, but cannot work on v4.26.0. The problem is about Problem 3 the theorem. I don't know why.

[Nick_adfor]

Oh... Terrible that PR is closed...

[Yuval Filmus]

I will redo the PR in a little bit — first my current Chebyshev.lean PR needs to get approved, then I will move it to a new directory, and then I will start adding the new files — hopefully this won't take too long.
Much of what you did is complementary.

[Johan Commelin]

Which PR is your current PR? You can link it like this: #12345

[Yuval Filmus]

My current PR is #32360 — waiting for it to be approved and merged.
My old PR is #31011. I am currently working on changing all the names and shortening all the proofs.

The old PR has several lemmas in other files which have already been merged into Mathlib.
In addition, there are two files, Basic.lean and Monic.lean.
The file Basic.lean contains several corollaries of results from #32360 which I will put into the current Chebyshev.lean (which will be moved to a directory Chebyshev and renamed Basic.lean).
In addition, it contains results about boundedness; zeroes of T and U; and extremas of T. I'm not sure whether all of these should be put in the same file or not.
All of these results are over the reals, but some of them (zeroes of T and U) also hold over the complex numbers — I can do this in the future.
Also, the result imply that all roots are single, a result which appears in Nick_adfor's work, and is probably also an easy corollary.
The results in Monic.lean are an extremal property of the Chebyshev polynomials, which can stay in one file (but the proofs will be reworked).

[Nick_adfor]

My previous post is here #new members > Formalize with Chebyshev polynomial.

[Nick_adfor]

There's really a terrible picture. If it can be more beautiful, the PRs will be easier to check.

[ A_symmetric ] ───▶ [ A_map_isHermitian ] ───▶ [ A_n_eigenvalues_real_C ]

[ charpoly_recursion ] ─┐
                        ├──▶ [ charpoly_A_eq_ChebyshevU ] ─┐
[ Chebyshev_U_recursion ] ┘                               │
                                                          ├──▶ [ A_n_eigenvalues_distinct ]
[ Chebyshev_U_simple_roots ] ─────────────────────────────┘

[Nick_adfor]

#29476 might still be useful

[Yuval Filmus]

The move is #32912.
Unfortunately my git skills are too weak to add the "deprecated module" PR.
Git is probably the least user friendly software on earth in common use.

[Nick_adfor]

I've never really learned how to efficiently use GitHub:( also PR:(((

[Yuval Filmus]

The deprecation is #32913, though I wonder if I did it correctly.

[Snir Broshi]

Yuval Filmus said:

Git is probably the least user friendly software on earth in common use.

Obligatory xkcd https://xkcd.com/1597/

[Ruben Van de Velde]

Unfortunately you now have a merge conflict. It might have been easier to wait with the second pr until the first had landed

[Snir Broshi]

I think a rebase rather than a merge might solve the conflict automatically

[Snir Broshi]

if not then a rebase with more params will

git switch MoveChebyshev2
git rebase --onto master MoveChebyshev
git push --force-with-lease

[Yuval Filmus]

Now it complains that the deprecated module cannot be found in Mathlib.lean, but if I add it, it complains that it cannot find it since it's a directory!

[Yuval Filmus]

I will just give up.
If only experts can do it, only experts should do it.

[Yuval Filmus]

Does the documentation on the web cover issues such as (1) how to work with PRs that depend on each other (what is a recommended workflow wrt branching), (2) how to deprecate definitions and modules?
If not, it would be good to add it so that the rest of us can also contribute to Mathlib...

[Dagur Asgeirsson]

Yuval Filmus said:

Now it complains that the deprecated module cannot be found in Mathlib.lean, but if I add it, it complains that it cannot find it since it's a directory!

If you follow the suggestion I just added on #32913, does it work to add the import to Mathlib.lean?

[Dagur Asgeirsson]

Yuval Filmus said:

Does the documentation on the web cover issues such as (1) how to work with PRs that depend on each other (what is a recommended workflow wrt branching), (2) how to deprecate definitions and modules?
If not, it would be good to add it so that the rest of us can also contribute to Mathlib...

• If you start typing deprecated in VSCode, for me three suggestions pop up, deprecated, deprecated alias, and deprecated module. If I pick one, it automatically generates the correct syntax. Did you try this?
• There is a script scripts/add_deprecations.sh that automatically adds deprecations. I think it doesn't detect changes of namespaces though (e.g. if Foo is changed to Bar, and baz is defined inside the Foo namespace which is then changed to Bar, it doesn't deprecate Foo.baz).
• I had to manually add a bunch of deprecations in # #32746. I found that doing one example and then asking Claude to do the rest worked quite well.

[Yuval Filmus]

The problem is that this kind of tips aren't written anywhere, compared to the copious documentation of Lean itself.

[Dagur Asgeirsson]

Feel free to open a PR to the website improving the contribution guidelines, if you learn something useful. That's always welcome. Everyone is just doing their best with their limited time!

[Yuval Filmus]

No doubt, that's why I'm trying to highlight areas for improvement.
Hopefully in a little bit I will be able to write such a guide myself...
Meanwhile I will take a look at this: https://arxiv.org/pdf/2508.21593v1

[Yuval Filmus]

Dagur Asgeirsson said:

Yuval Filmus said:

Now it complains that the deprecated module cannot be found in Mathlib.lean, but if I add it, it complains that it cannot find it since it's a directory!

If you follow the suggestion I just added on #32913, does it work to add the import to Mathlib.lean?

Looks promising!