polynomial.comp_prod

Stream: Is there code for X?

[Damiano Testa]

Dear All,

I am struggling to find the lemma below: I tried library_search, suggest, hint, looking around in relevant files, all to no avail. I also tried seeing if the docs linkifier told me that my guessed name was the actual name, but also that failed! Can someone please tell me what the lemma is called?

Or explain to me that it is false, because I still do not understand what comp and prod do?

Thanks!

import data.polynomial.eval

open_locale polynomial big_operators

lemma polynomial.comp_prod {ι R : Type*} (s : finset ι) [comm_semiring R] (f : ι → R[X]) (p : R[X]) :
  (s.prod f).comp p = ∏ i in s, ((f i).comp p) :=
sorry

[Yaël Dillies]

This is becoming comical :grinning: docs#polynomial.prod_comp

[Yaël Dillies]

It's not quite what you ask for, but the glue belongs to the realm of big operators.

[Damiano Testa]

Seriously?!?!

[Damiano Testa]

Sometimes I wonder whether formalizing math is what I should be doing...

[Yaël Dillies]

Damiano, how are you looking for lemmas? My goto is the search bar in the online docs.

[Damiano Testa]

I mostly try the auto-complete, then I try stating the lemma in isolation and using library_search. Finally, I open files that appear relevant and do a mix of Ctrl+F and browsing.

[Damiano Testa]

Anyway, at least this time I have not been able to fill in the glue right away, but I'll try harder with the lemma that you suggested!

[Eric Rodriguez]

ctrl+shift+f in VSCode is always nice, and you can search by name in the docs which is also worth checking

[Damiano Testa]

In this specific case, I think that my inability has been hindered by my difficulty of converting betweem finsets and multisets. I can see that the lemma that Yaël linked is very close to what I want, I might have even glanced at it, but decided that I was unable to make it work, since it used multisets, instead of finsets.

[Damiano Testa]

Here is a follow up: how can I get Lean to construct the multiset image of the finset s under the map f?

[Damiano Testa]

and I hope that the answer is not finset.image.to_multiset or something like this!

[Damiano Testa]

(let me try that right away!)

[Kevin Buzzard]

wait what is the construction you want? Does the constant function send {1,2} to {x} or {x,x}? If you change a finset to a multiset you'll not get duplicates of course.

[Damiano Testa]

I was referring to the context of the lemma above: I have a finset of \iota, a map from \iota to another type and I want the "multiset image" of the map. Thus, if the map is constant, I want a lot of the same elements in the multiset.

The source though has no repetitions.

[Damiano Testa]

that is, with more maths notations, I want $[f(i) : i \in s]$ as a multiset, since this is what I need to feed to the lemma that Yaël suggested.

[Damiano Testa]

Kevin, in your example, I would want $\{x,x\}$.

[Yaël Dillies]

A finset is definitionally a multiset. finset.prod s f is definitionally (multiset.map s f).prod.

[Damiano Testa]

Yaël, thanks! I had not tried forcing Lean to accept it: this is not elegant, but works!

lemma polynomial.comp_prod {ι R : Type*} (s : finset ι) [comm_semiring R] (f : ι → R[X]) (p : R[X]) :
  (s.prod f).comp p = ∏ i in s, ((f i).comp p) :=
by {
  convert polynomial.prod_comp _ _,
  ext,
  simp,
  refl,
}

[Damiano Testa]

I had tried rw which failed, but I had not tried convert, since I was not hoping for defeqs!

[Damiano Testa]

Should this lemma then go into mathlib?

[Yaël Dillies]

It doesn't seem to me that we've yet decided how much duplication between multiset.prod and finset.prod we want.

[Yaël Dillies]

Actually, you should be able to golf the above to one line without a convert. What does (polynomial.prod_comp _ _).trans $ by library_search produce?

[Damiano Testa]

Sorry, I'm taking a break! Will report once I'm back!

[Damiano Testa]

I tried it now and it times out. However, library_search often seems to time out for me...

[Eric Rodriguez]

Yaël Dillies said:

Actually, you should be able to golf the above to one line without a convert. What does (polynomial.prod_comp _ _).trans $ by library_search produce?

by simpa works at the end, but I think I made people unhappy when I admitted I used simpa for simp+refl

[Damiano Testa]

This is also a proof:

lemma polynomial.comp_prod {ι R : Type*} (s : finset ι) [comm_semiring R] (f : ι → R[X]) (p : R[X]) :
  (s.prod f).comp p = ∏ i in s, ((f i).comp p) :=
begin
  refine (polynomial.prod_comp _ _).trans _,
  refine ext (λ (n : ℕ), _),
  rw [multiset.map_map],
-- here the goal is
-- (multiset.map ((λ (q : R[X]), q.comp p) ∘ f) s.val).prod.coeff n = (∏ (i : ι) in s, (f i).comp p).coeff n
-- and the following refl proves it
  refl,
end