Reasoning with `mv_polynomial` monomials

Stream: new members

[Hanting Zhang]

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.

[Eric Wieser]

Sorry for leading you into that trap!

[Eric Wieser]

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]

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]

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]

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.