## Stream: new members

### Topic: Reasoning with mv_polynomial monomials

#### 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 nth 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.

#### Eric Wieser (Jan 20 2021 at 19:21):

Sorry for leading you into that trap!

#### 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


#### 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

#### 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


#### 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