Zulip Chat Archive

Stream: maths

Topic: chebyshev polynomials


Johan Commelin (Sep 25 2020 at 08:36):

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 (Sep 25 2020 at 08:37):

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

Violeta Hernández (Aug 01 2022 at 20:42):

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

Violeta Hernández (Aug 01 2022 at 20:43):

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 (Aug 01 2022 at 20:44):

(deleted)

Violeta Hernández (Aug 01 2022 at 20:46):

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

Violeta Hernández (Aug 01 2022 at 20:48):

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

Violeta Hernández (Aug 01 2022 at 20:51):

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 (Aug 01 2022 at 21:14):

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 (Aug 02 2022 at 06:22):

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

Violeta Hernández (Aug 02 2022 at 11:05):

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

Violeta Hernández (Aug 02 2022 at 11:07):

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

Kevin Buzzard (Aug 02 2022 at 11:41):

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

Kevin Buzzard (Aug 02 2022 at 11:42):

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 (Aug 02 2022 at 12:08):

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 (Aug 02 2022 at 12:19):

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

Kevin Buzzard (Aug 02 2022 at 12:20):

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 (Aug 02 2022 at 12:21):

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 (Aug 02 2022 at 12:22):

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 (Aug 02 2022 at 12:22):

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 (Aug 02 2022 at 12:24):

For this particular question ;-)

Damiano Testa (Aug 02 2022 at 12:24):

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

Yaël Dillies (Aug 02 2022 at 12:24):

The plan is for them to be, though.

Damiano Testa (Aug 02 2022 at 12:24):

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 (Aug 02 2022 at 12:26):

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 (Aug 02 2022 at 12:31):

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 (Aug 02 2022 at 12:31):

For the record, this works, though:

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

:smile:

Damiano Testa (Aug 02 2022 at 12:34):

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 (Aug 02 2022 at 12:38):

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 (Aug 02 2022 at 12:38):

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

Damiano Testa (Aug 02 2022 at 12:38):

Even more: it is simp.

Yaël Dillies (Aug 02 2022 at 12:39):

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

Damiano Testa (Aug 02 2022 at 12:42):

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 (Aug 02 2022 at 12:42):

look at the show_term for 200 on both

Eric Rodriguez (Aug 02 2022 at 12:44):

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 (Aug 02 2022 at 12:49):

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

Damiano Testa (Aug 02 2022 at 12:50):

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

Damiano Testa (Aug 02 2022 at 12:52):

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 (Aug 02 2022 at 13:05):

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 (Aug 02 2022 at 13:14):

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

Eric Wieser (Aug 02 2022 at 14:03):

That's the same for submodules, right?

Kevin Buzzard (Aug 02 2022 at 17:41):

So what factional ideal is that??

Kevin Buzzard (Aug 02 2022 at 17:42):

The identity I guess?

Eric Rodriguez (Aug 02 2022 at 18:20):

all of them are 1 yeah

Violeta Hernández (Aug 03 2022 at 05:58):

What will Lean4 use instead of the bits?

Eric Wieser (Aug 03 2022 at 07:22):

docs4#OfNat or similar

Wrenna Robson (Aug 03 2022 at 08:37):

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


Last updated: Dec 20 2023 at 11:08 UTC