Zulip Chat Archive

Stream: new members

Topic: Help with mv_polynomial


María Inés de Frutos Fernández (Sep 07 2022 at 17:35):

I'm having trouble using the new mv_polynomial.prod_X_add_C_coeff. What would I have to use instead of the last rw in this mwe?

import ring_theory.polynomial.vieta

open polynomial
lemma polynomial.prod_X_sub_C_coeff {K : Type*} [field K]  {n : } (hn : 0 < n) (b : fin n  K)
  {m : } (hm : m  n) : (finprod (λ (k : fin n), polynomial.X - (polynomial.C (b k)))).coeff m =
  (finset.powerset_len (n - m) finset.univ).sum
    (λ (t : finset (fin n)), t.prod (λ (i : (fin n)), - b i)) :=
begin
  simp_rw [sub_eq_add_neg,  polynomial.C_neg,  pi.neg_apply],
  rw [finprod_eq_prod_of_fintype],
  rw mv_polynomial.prod_X_add_C_coeff, -- now fails because the LHS of this lemma has changed
  sorry
end

Adam Topaz (Sep 07 2022 at 19:39):

docs#mv_polynomial.prod_X_add_C_coeff

Adam Topaz (Sep 07 2022 at 19:40):

It seems like the goal at that point is

(finset.univ.prod (λ (i : fin n), X + C ((-b) i))).coeff m =
  (finset.powerset_len (n - m) finset.univ).sum (λ (x : finset (fin n)), x.prod (λ (x : fin n), (-b) x))

and the LHS doesn't match the LHS of the lemma because of the -b (as opposed to mv_polynomial.X).
Am I just confused?

María Inés de Frutos Fernández (Sep 07 2022 at 19:54):

Yes, that's what's going on - the old prod_X_add_C_coeff, which was modified to mv_polynomial.prod_X_add_C_coeff in #15008, was

lemma prod_X_add_C_coeff (r : σ  R) (k : ) (h : k  card σ):
  polynomial.coeff ( i : σ, (polynomial.C (r i) + polynomial.X)) k =
   t in powerset_len (card σ - k) (univ : finset σ),  i in t, r i :=

The new version seems more general, but I can't figure out how to apply it to prove the goal above.

Xavier Roblot (Sep 07 2022 at 20:11):

For this kind of situation, you might want to use the new docs#multiset.prod_X_sub_C_coeff which is more flexible.

María Inés de Frutos Fernández (Sep 07 2022 at 20:15):

Ok, I'll check it out. Thanks!

Junyan Xu (Sep 08 2022 at 03:15):

@María Inés de Frutos Fernández You can prove it this way:

import ring_theory.polynomial.vieta

lemma finset.esymm_map_val {σ R} [comm_semiring R] (f : σ  R) (s : finset σ) (n : ) :
  (s.val.map f).esymm n = (s.powerset_len n).sum (λ t, t.prod f) :=
begin
  rw [multiset.esymm, multiset.powerset_len_map,  finset.map_val_val_powerset_len],
  simpa only [multiset.map_map],
end

open polynomial
lemma polynomial.prod_X_sub_C_coeff {K : Type*} [field K]  {n : } (hn : 0 < n) (b : fin n  K)
  {m : } (hm : m  n) : (finprod (λ (k : fin n), polynomial.X - (polynomial.C (b k)))).coeff m =
  (finset.powerset_len (n - m) finset.univ).sum
    (λ (t : finset (fin n)), t.prod (λ (i : (fin n)), - b i)) :=
begin
  simp_rw [sub_eq_add_neg,  polynomial.C_neg,  pi.neg_apply],
  rw [finprod_eq_prod_of_fintype],
  rw finset.prod_eq_multiset_prod,
  rw  multiset.map_map (λ x : K, X + C x) (-b),
  have : (finset.univ.val.map (-b)).card = n,
  { rw multiset.card_map, exact finset.card_fin n },
  rw multiset.prod_X_add_C_coeff,
  { rw finset.esymm_map_val, congr, exact this },
  { rw this, exact hm },
end

Junyan Xu (Sep 08 2022 at 03:15):

I've PR'd the lemma finset.esymm_map_val and use it to golf an existing proof: #16424

María Inés de Frutos Fernández (Sep 08 2022 at 08:29):

Thanks!


Last updated: Dec 20 2023 at 11:08 UTC