chebyshev polynomials

Stream: maths

[Johan Commelin]

branch#chebpoly is a little experiment that I did for fun. And it turned out to be a lot of fun!
It's 350 lines of code where I mix polynomials, trigonometric functions and zmod p.

Everything fit pretty smoothly together, but it will need some cleaning up before it can be PR'd. In particular, it would benefit from having #4241 and #4197 merged.

The end result is that we get a family of polynomials over Z, that commute with each other, and such that the p-th polynomial is congruent to X ^ p modulo p.

[Johan Commelin]

Such a family is a Lambda structure, and there are only two such structures on polynomial int.

[Violeta Hernández]

On the topic of Chebyshev polynomials, I wanted to ask about the design

[Violeta Hernández]

Chebyshev polynomials have the property that 2*T(x/2) and U(x/2) are monic and have integer coefficients (save for 2*T₀(x/2) = 2), and I need to use this first fact to prove Niven's theorem

[Violeta Hernández]

(deleted)

[Violeta Hernández]

There are recursive formulas for these half-Chebyshev polynomials, which means they can be defined independently of the others

[Violeta Hernández]

So, it seems kind of tempting to redefine, at the very least, U in terms of the half-version

[Violeta Hernández]

Most likely this is a bad idea, since I imagine the recursive characterization of these polynomials is easier to work with, but I still wanted to bring up that idea

[Violeta Hernández]

The most conservative and probably best approach would be to define T_half and U_half via their own recursive definitions, and prove the equivalences

[Julian Külshammer]

Did you see that there are also docs#polynomial.dickson, which might be (related to) what you want?

[Violeta Hernández]

Oh nice! I didn't know about these. dickson 1 1 is exactly what I want.

[Violeta Hernández]

Related question, is C 2 * X really the simp-normal form? I expected monomial 1 2.

[Kevin Buzzard]

I would expect 2 * X, that's surely the mathematician-normal form

[Kevin Buzzard]

I would of thought that 2 * X was the most ring-friendly form, for example. Perhaps it depends a lot on what you're doing?

[Damiano Testa]

A lot of lemmas about polynomials benefit from maintaining a distinction between the stuff that comes from the ground ring and the stuff that is inherently a polynomial. Using C helps maintaining such a distinction. For a fun exercise, try filling in the two sorries

example {R} [semiring R] : nat_degree (200 : R[X]) = 0 :=
begin
  sorry
end

example {R} [semiring R] : nat_degree (C (200 : R)) = 0 :=
begin
  sorry
end

and see which one is easier!

[Violeta Hernández]

Isn't nat_degree n = 0 for any integer n? Surely that's already proven

[Kevin Buzzard]

Does 2 really come from the ground ring though? My gut feeling is that it comes from the fundamental nat action on an additive abelian group, which is embedded in mathlib way before polynomials appear. Which is easier to prove, 2 * X = X + X or (C 2) * X = X + X? ring will nail the former, and perhaps abel too.

[Damiano Testa]

Sure, 2 comes from bit0/1 and this also causes further issues. I was addressing the reason why C appears, not specifically with numerals.

[Kevin Buzzard]

My guess is that this is a situation where the question of you want the normal form to be depends on what you're doing, so there's no "best" answer to what the simp normal form should be. If you're proving stuff about all polynomials by induction then monomial is going to show up, for example

[Damiano Testa]

Indeed, you can prove the nat_degree (numeral) by repeated application of bit0 and bit1 and going forwards, but there is no type of numerals, as far as I know. Whereas, assuming that something has the shape C _ is much easier to deal with.

[Kevin Buzzard]

For this particular question ;-)

[Damiano Testa]

Also, 200 : R[X] is not the same as ((200 : ℕ) : R[X]).

[Yaël Dillies]

The plan is for them to be, though.

[Damiano Testa]

This is the plan, yes, and I think that Anne is working on this. I am also told that Lean4 will no longer have bit0/1, so this is also a transient issue.

[Damiano Testa]

Kevin Buzzard said:

For this particular question ;-)

Agreed, although a lot of the API revolves around having lemmas for C whereas lemmas about "a term arising from repeated application of bit0/1 starting from 0, 1" are... rare!

[Damiano Testa]

Violeta Hernández said:

Isn't nat_degree n = 0 for any integer n? Surely that's already proven

Actually, the lemma with the coercion from nat to R[X] is in the library (docs#polynomial.nat_degree_nat_cast). This lemma, however, needs to be forced through to prove the given example:

example {R} [semiring R] : nat_degree (200 : R[X]) = 0 :=
begin
  convert nat_degree_nat_cast 200,
  simp only [nat.cast_bit0, nat.cast_bit1, nat.cast_one],
end

You can see that simp goes via bit0/1.

[Damiano Testa]

For the record, this works, though:

example {R} [semiring R] : nat_degree (C (200 : R)) = 0 :=
nat_degree_C _

:smile:

[Damiano Testa]

Ultimately, the issue is that it is hard to quantify over all possible ways in which nat, int, R,... fit inside R[X] and C conveniently deals with a lot of cases.

[Damiano Testa]

For the record, the simp-normal form does remove the C:

example {R} [semiring R] : nat_degree (C (200 : R) * X) = 0 :=
by {simp,  --  ⊢ (200 * X).nat_degree = 0
}

[Yaël Dillies]

Surely simp only [nat.cast_bit0, nat.cast_bit1, nat.cast_one] is just norm_num?

[Damiano Testa]

Even more: it is simp.

[Yaël Dillies]

Surely norm_num is faster here. simp is a kitchen sink tactic.

[Damiano Testa]

With 200 it is hard to notice a difference, here simp takes about a second, while norm_num is essentially instantaneous:

example {R} [semiring R] : (2000000 : R[X]) = (2000000 : ℕ) :=
begin
  simp,
end

example {R} [semiring R] : (2000000 : R[X]) = (2000000 : ℕ) :=
begin
  norm_num,
end

[Eric Rodriguez]

look at the show_term for 200 on both

[Eric Rodriguez]

the difference comes down to docs#nat.cast_bit0 and docs#norm_num.nat_cast_bit0, the first one needs rws but the second one can literally just be basically an apply chain

[Kevin Buzzard]

Are bit0 and bit1 ever used for anything other than numerals?

[Damiano Testa]

My point stands, though: with C you can often get away with not needing either simp or norm_num.

[Damiano Testa]

Technically, bit0 only needs an addition and bit1 also a one. Once these are in place, you have "numerals". I do not know of any "exotic" situations where you use bit0/1 in a context where "seeing numbers" would seem strange.

[Eric Rodriguez]

import ring_theory.fractional_ideal

open_locale polynomial non_zero_divisors

variables {R : Type*} [comm_ring R]

example : fractional_ideal (R⁰) (fraction_ring R) := 37

[Eric Rodriguez]

(note that bit0 is id and bit1 1 = 1)

[Eric Wieser]

That's the same for submodules, right?

[Kevin Buzzard]

So what factional ideal is that??

[Kevin Buzzard]

The identity I guess?

[Eric Rodriguez]

all of them are 1 yeah

[Violeta Hernández]

What will Lean4 use instead of the bits?

[Eric Wieser]

docs4#OfNat or similar

[Wrenna Robson]

I've used bit0 and bit1 for things before that weren't numerals.