prod_multiset_count

Stream: general

[Johan Commelin]

import algebra.big_operators

open_locale big_operators
open_locale classical

lemma finset.prod_multiset_count {M : Type*} [comm_monoid M] (s : multiset M) :
  s.prod = ∏ m in s.to_finset, m ^ (s.count m) :=
sorry

What's the best way to prove this?

[Alex J. Best]

Via a multiset is the union of repeat a (count S a) for a \in S?

[Johan Commelin]

Maybe... I haven't spent that much time on this yet.

[Johan Commelin]

I was just annoyed that it doesn't seem to be in the library yet... (-;

[Alex J. Best]

I couldn't even find Union of a set/list of multisets?

[Chris Hughes]

It's called bind.

[Kevin Buzzard]

That's surely only a Union of a multiset of multisets?

[Amelia Livingston]

here's emphatically not the best way to prove it

[Kevin Buzzard]

Aah induction on the size of the corresponding finset. This reminds me of something that I don't know how to do. Amelia has added {n : ℕ} (hn : s.to_finset.card = n) as extra inputs to her proof, and in practice you will be able to give rfl as the hn input and not worry. If you're in the middle of some complicated thing and suddenly decide that you want to do induction on the length of a list, what do you do?

import data.list.basic

-- how to do induction on the length of a list?
example (α : Type) (L : list α) (P : list α → Prop)
(h0 : P []) (h1 : ∀ n : ℕ,
  (∀ L: list α, L.length = n → P L) → (∀ L : list α, L.length = (n + 1) → P L)) :
  ∀ L : list α, P L :=
begin
  intro L,
  set n := L.length with hn,
  induction n with d hd, -- induction tactic failed, failed to create new goal

end

We could prove an auxiliary lemma with the extra input of a natural which is equal to the length of L, and then use that auxiliary lemma, but is there a way to do it without having to "start again" as it were?

[Sebastien Gouezel]

You can see an example in https://github.com/leanprover-community/mathlib/blob/53c15319008e3a11d5e8f6c90b64cb0b68f03fa1/src/analysis/normed_space/finite_dimension.lean#L79

[Sebastien Gouezel]

Or in a recent PR by @Kenny Lau
https://github.com/leanprover-community/mathlib/blob/cefc8c85895d5acdf79c659edec5fbc1d513b13b/src/field_theory/splitting_field.lean#L209

[Kenny Lau]

import algebra.big_operators

open_locale big_operators
open_locale classical

open multiset finset

lemma finset.prod_multiset_count {M : Type*} [comm_monoid M] (s : multiset M) :
  s.prod = ∏ m in s.to_finset, m ^ (s.count m) :=
begin
  apply s.induction_on, { rw [prod_zero, to_finset_zero, prod_empty] },
  intros a s ih, by_cases has : a ∈ s.to_finset,
  { rw [prod_cons, to_finset_cons, insert_eq_of_mem has, ih,
      ← insert_erase has, prod_insert (not_mem_erase _ _), prod_insert (not_mem_erase _ _),
      ← mul_assoc, count_cons_self, pow_succ],
    congr' 1, refine prod_congr rfl (λ x hx, _), rw [count_cons_of_ne (ne_of_mem_erase hx)] },
  rw [prod_cons, to_finset_cons, prod_insert has, count_cons_self],
  rw mem_to_finset at has, rw [count_eq_zero_of_not_mem has, pow_one], congr' 1,
  rw ih, refine prod_congr rfl (λ x hx, _), rw mem_to_finset at hx, rw count_cons_of_ne,
  rintro rfl, exact has hx
end

[Kevin Buzzard]

import data.list.basic

open list

example (α : Type) (L : list α) (P : list α → Prop)
(h0 : P []) (h1 : ∀ n : ℕ,
  (∀ L: list α, L.length = n → P L) → (∀ L : list α, L.length = (n + 1) → P L)) :
  ∀ L : list α, P L :=
begin
  intro L,
  unfreezingI {induction h : L.length with d hd generalizing L},
  { convert h0, rwa length_eq_zero at h},
  { apply h1 d, assumption, assumption}
end

I did my homework

[Mario Carneiro]

By the way src#multiset.to_finset_sum_count_eq looks pretty similar to what is needed here

[Mario Carneiro]

src#multiset.le_smul_erase_dup also does something similar