Zulip Chat Archive

Stream: new members

Topic: Reasoning with `mv_polynomial` monomials


view this post on Zulip Hanting Zhang (Jan 20 2021 at 18:50):

Hi, are there any lemmas that can finish this problem easily?

import tactic
import data.mv_polynomial.rename
import data.mv_polynomial.comm_ring

open equiv (perm) finset
open_locale big_operators
noncomputable theory

namespace mv_polynomial
variables (σ : Type*) (R : Type*) [comm_semiring R] [fintype σ]

/-- The `n`th elementary symmetric `mv_polynomial σ R`. -/
def esymm (n : ) : mv_polynomial σ R :=
 t in powerset_len n univ,  i in t, X i

lemma esymm_eq_sum_monomial (n : ) : esymm σ R n =
   t in powerset_len n univ, monomial ( i in t, finsupp.single i 1) 1 :=
begin
  refine sum_congr rfl (λ x hx, _), -- is there anything that tells Lean the goal here is obvious?
  rw monic_monomial_eq,
  rw finsupp.prod,
  sorry
end

end mv_polynomial

I found similar lemmas in mathlib, but none that really give me what I'm looking for.

view this post on Zulip Eric Wieser (Jan 20 2021 at 19:21):

Sorry for leading you into that trap!

view this post on Zulip Eric Wieser (Jan 20 2021 at 19:30):

I can make some progress with

lemma esymm_eq_sum_monomial (n : ) : esymm σ R n =
   t in powerset_len n univ, monomial ( i in t, finsupp.single i 1) 1 :=
begin
  refine sum_congr rfl (λ x hx, _), -- is there anything that tells Lean the goal here is obvious?
  rw monic_monomial_eq,
  rw finsupp.prod_pow,
  rw  prod_subset (λ y _, finset.mem_univ y : x  univ) (λ y _ hy, _),
  { refine prod_congr rfl (λ x' hx', _),
    convert (pow_one _).symm,
    sorry, },
  { convert (pow_zero _),
    sorry },
end

view this post on Zulip Eric Wieser (Jan 20 2021 at 19:42):

This type of problem embodies everything I hate about finset / finsupp - there are just too many ways to express sums over things, and a huge pile of the NxM lemmas for N different ways to sum over M types are missing

view this post on Zulip Eric Wieser (Jan 20 2021 at 19:44):

Here's a full but ugly proof:

lemma esymm_eq_sum_monomial (n : ) : esymm σ R n =
   t in powerset_len n univ, monomial ( i in t, finsupp.single i 1) 1 :=
begin
  refine sum_congr rfl (λ x hx, _), -- is there anything that tells Lean the goal here is obvious?
  rw monic_monomial_eq,
  rw finsupp.prod_pow,
  rw  prod_subset (λ y _, finset.mem_univ y : x  univ) (λ y _ hy, _),
  { refine prod_congr rfl (λ x' hx', _),
    convert (pow_one _).symm,
    convert (finsupp.apply_add_hom x' : (σ →₀ ) →+ ).map_sum _ x,
    classical,
    simp [finsupp.single_apply, finset.filter_eq', apply_ite, apply_ite finset.card],
    rw if_pos hx', },
  { convert (pow_zero _),
    convert (finsupp.apply_add_hom y : (σ →₀ ) →+ ).map_sum _ x,
    classical,
    simp [finsupp.single_apply, finset.filter_eq', apply_ite, apply_ite finset.card],
    rw if_neg hy, },
end

view this post on Zulip Hanting Zhang (Jan 20 2021 at 20:48):

Don't worry about it, thanks for the proof! This seems generally useful, so I'll be reworking it into a more general lemma for converting between finsupp and finset, if you don't mind.

And I do agree that sums are not very fun in Lean. The more I work the more I just want to drop everything and start proving "trivial" conversions like powerset_len univ n to {s : s.card = n}, etc, etc.


Last updated: May 18 2021 at 16:25 UTC