Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
! This file was ported from Lean 3 source module algebra.big_operators.multiset.basic
! leanprover-community/mathlib commit 6c5f73fd6f6cc83122788a80a27cdd54663609f4
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.List.BigOperators.Basic
import Mathlib.Data.Multiset.Basic
/-!
# Sums and products over multisets
In this file we define products and sums indexed by multisets. This is later used to define products
and sums indexed by finite sets.
## Main declarations
* `Multiset.prod`: `s.prod f` is the product of `f i` over all `i ∈ s`. Not to be mistaken with
the cartesian product `Multiset.product`.
* `Multiset.sum`: `s.sum f` is the sum of `f i` over all `i ∈ s`.
## Implementation notes
Nov 2022: To speed the Lean 4 port, lemmas requiring extra algebra imports
(`data.list.big_operators.lemmas` rather than `.basic`) have been moved to a separate file,
`algebra.big_operators.multiset.lemmas`. This split does not need to be permanent.
-/
variable { ι α β γ : Type _ : Type (?u.120170+1)}
namespace Multiset
section CommMonoid
variable [ CommMonoid : Type ?u.13328 → Type ?u.13328 α ] { s t : Multiset α } { a : α } { m : Multiset ι } { f g : ι → α }
/-- Product of a multiset given a commutative monoid structure on `α`.
`prod {a, b, c} = a * b * c` -/
@[ to_additive
"Sum of a multiset given a commutative additive monoid structure on `α`.
`sum {a, b, c} = a + b + c`"]
def prod : Multiset α → α :=
foldr (· * ·) ( fun x y z => by (fun x x_1 => x * x_1 ) x ((fun x x_1 => x * x_1 ) y z ) = (fun x x_1 => x * x_1 ) y ((fun x x_1 => x * x_1 ) x z ) simp [ mul_left_comm ] ) 1
#align multiset.prod Multiset.prod
#align multiset.sum Multiset.sum
@[ to_additive ]
theorem prod_eq_foldr : ∀ (s : Multiset α prod s = foldr (fun x x_1 => x * x_1 ) (_ : ∀ (x y z : α ), x * (y * z = y * (x * z ) 1 s prod_eq_foldr ( s : Multiset α ) :
prod s = foldr (· * ·) ( fun x y z => by (fun x x_1 => x * x_1 ) x ((fun x x_1 => x * x_1 ) y z ) = (fun x x_1 => x * x_1 ) y ((fun x x_1 => x * x_1 ) x z ) simp [ mul_left_comm ] ) 1 s :=
rfl : ∀ {α : Sort ?u.2992} {a : α }, a = a
#align multiset.prod_eq_foldr Multiset.prod_eq_foldr
#align multiset.sum_eq_foldr Multiset.sum_eq_foldr
@[ to_additive ]
theorem prod_eq_foldl ( s : Multiset α ) :
prod s = foldl (· * ·) ( fun x y z => by (fun x x_1 => x * x_1 ) ((fun x x_1 => x * x_1 ) x y ) z = (fun x x_1 => x * x_1 ) ((fun x x_1 => x * x_1 ) x z ) y simp [ mul_right_comm ] ) 1 s :=
( foldr_swap : ∀ {α : Type ?u.4209} {β : Type ?u.4210} (f : α → β → β H : LeftCommutative f b : β ) (s : Multiset α foldr f H b s = foldl (fun x y => f y x ) (_ : ∀ (_x : β ) (_y _z : α ), f _z (f _y _x = f _y (f _z _x ) b s _ : ?m.4211 → ?m.4212 → ?m.4212
_ _ _ ). trans : ∀ {α : Sort ?u.4217} {a b c : α }, a = b b = c a = c trans ( by foldl (fun x y => y * x ) (_ : ∀ (_x _y _z : α ), _z * (_y * _x = _y * (_z * _x ) 1 s = foldl (fun x x_1 => x * x_1 ) (_ : ∀ (x y z : α ), x * y * z = x * z * y ) 1 s simp [ mul_comm ] )
#align multiset.prod_eq_foldl Multiset.prod_eq_foldl
#align multiset.sum_eq_foldl Multiset.sum_eq_foldl
@[ to_additive ( attr := simp , norm_cast )]
theorem coe_prod ( l : List α ) : prod ↑ l = l . prod : {α : Type ?u.4999} → [inst : Mul α [inst : One α List α α :=
prod_eq_foldl _
#align multiset.coe_prod Multiset.coe_prod
#align multiset.coe_sum Multiset.coe_sum
@[ to_additive ( attr := simp )]
theorem prod_toList ( s : Multiset α ) : s . toList . prod : {α : Type ?u.6149} → [inst : Mul α [inst : One α List α α = s . prod := by
conv_rhs => rw [ ← coe_toList s ]
rw [ coe_prod ]
#align multiset.prod_to_list Multiset.prod_toList
#align multiset.sum_to_list Multiset.sum_toList
@[ to_additive ( attr := simp )]
theorem prod_zero : @ prod α _ 0 = 1 :=
rfl : ∀ {α : Sort ?u.7677} {a : α }, a = a
#align multiset.prod_zero Multiset.prod_zero
#align multiset.sum_zero Multiset.sum_zero
@[ to_additive ( attr := simp )]
theorem prod_cons ( a : α ) ( s ) : prod ( a ::ₘ s ) = a * prod s :=
foldr_cons _ : ?m.8604 → ?m.8605 → ?m.8605
_ _ _ _
#align multiset.prod_cons Multiset.prod_cons
#align multiset.sum_cons Multiset.sum_cons
@[ to_additive ( attr := simp )]
theorem prod_erase [ DecidableEq : Sort ?u.8725 → Sort (max1?u.8725) α ] ( h : a ∈ s ) : a * ( s . erase a ). prod = s . prod := by
rw [ ← s . coe_toList , coe_erase , coe_prod , coe_prod , List.prod_erase ( mem_toList . 2 : ∀ {a b : Prop }, (a ↔ b b → a h ) ]
#align multiset.prod_erase Multiset.prod_erase
#align multiset.sum_erase Multiset.sum_erase
@[ to_additive ( attr := simp )]
theorem prod_map_erase [ DecidableEq : Sort ?u.10099 → Sort (max1?u.10099) ι ] { a : ι } ( h : a ∈ m ) :
f a * (( m . erase a ). map f ). prod = ( m . map f ). prod := by
rw [ ← m . coe_toList , coe_erase , coe_map , coe_map , coe_prod , coe_prod ,
List.prod_map_erase f ( mem_toList . 2 : ∀ {a b : Prop }, (a ↔ b b → a h ) ]
#align multiset.prod_map_erase Multiset.prod_map_erase
#align multiset.sum_map_erase Multiset.sum_map_erase
@[ to_additive ( attr := simp )]
theorem prod_singleton : ∀ (a : α ), prod {a } = a prod_singleton ( a : α ) : prod { a } = a := by
simp only [ mul_one , prod_cons , ← cons_zero : ∀ {α : Type ?u.11671} (a : α ), a ::ₘ 0 = {a } , eq_self_iff_true : ∀ {α : Sort ?u.11684} (a : α ), a = a ↔ True , prod_zero ]
#align multiset.prod_singleton Multiset.prod_singleton
#align multiset.sum_singleton Multiset.sum_singleton
@[ to_additive ]
theorem prod_pair ( a b : α ) : ({ a , b } : Multiset α ). prod = a * b := by
rw [ insert_eq_cons , prod_cons , prod_singleton ]
#align multiset.prod_pair Multiset.prod_pair
#align multiset.sum_pair Multiset.sum_pair
@[ to_additive ( attr := simp )]
theorem prod_add ( s t : Multiset α ) : prod ( s + t ) = prod s * prod t :=
Quotient.inductionOn₂ s t fun l₁ l₂ => by simp
#align multiset.prod_add Multiset.prod_add
#align multiset.sum_add Multiset.sum_add
theorem prod_nsmul ( m : Multiset α ) : ∀ n : ℕ , ( n • m ). prod = m . prod ^ n
| 0 => by
rw [ zero_nsmul , pow_zero : ∀ {M : Type ?u.18586} [inst : Monoid M a : M ), a ^ 0 = 1 ]
rfl
| n + 1 => by rw [ add_nsmul : ∀ {A : Type ?u.18952} [inst : AddMonoid A a : A ) (m n : ℕ ), (m + n • a = m • a + n • a , one_nsmul , pow_add : ∀ {M : Type ?u.19034} [inst : Monoid M a : M ) (m n : ℕ ), a ^ (m + n = a ^ m * a ^ n , pow_one : ∀ {M : Type ?u.19079} [inst : Monoid M a : M ), a ^ 1 = a , prod_add , prod_nsmul m n ]
#align multiset.prod_nsmul Multiset.prod_nsmul
@[ to_additive ( attr := simp )]
theorem prod_replicate ( n : ℕ ) ( a : α ) : ( replicate n a ). prod = a ^ n := by
simp [ replicate , List.prod_replicate ]
#align multiset.prod_replicate Multiset.prod_replicate
#align multiset.sum_replicate Multiset.sum_replicate
@[ to_additive ]
theorem prod_map_eq_pow_single [ DecidableEq : Sort ?u.22682 → Sort (max1?u.22682) ι ] ( i : ι )
( hf : ∀ (i' : ι ), i' ≠ i i' ∈ m f i' = 1 hf : ∀ ( i' ) ( _ : i' ≠ i ), i' ∈ m → f i' = 1 ) : ( m . map f ). prod = f i ^ m . count i := by
induction' m using Quotient.inductionOn with l
simp [ List.prod_map_eq_pow_single i f hf ]
#align multiset.prod_map_eq_pow_single Multiset.prod_map_eq_pow_single
#align multiset.sum_map_eq_nsmul_single Multiset.sum_map_eq_nsmul_single
@[ to_additive ]
theorem prod_eq_pow_single [ DecidableEq : Sort ?u.29728 → Sort (max1?u.29728) α ] ( a : α ) ( h : ∀ (a' : α ), a' ≠ a a' ∈ s a' = 1 h : ∀ ( a' ) ( _ : a' ≠ a ), a' ∈ s → a' = 1 ) :
s . prod = a ^ s . count a := by
induction' s using Quotient.inductionOn with l
simp [ List.prod_eq_pow_single a h ]
#align multiset.prod_eq_pow_single Multiset.prod_eq_pow_single
#align multiset.sum_eq_nsmul_single Multiset.sum_eq_nsmul_single
@[ to_additive ]
theorem pow_count [ DecidableEq : Sort ?u.36655 → Sort (max1?u.36655) α ] ( a : α ) : a ^ s . count a = ( s . filter ( Eq a )). prod := by
rw [ filter_eq , prod_replicate ]
#align multiset.pow_count Multiset.pow_count
#align multiset.nsmul_count Multiset.nsmul_count
@[ to_additive ]
theorem prod_hom [ CommMonoid : Type ?u.39820 → Type ?u.39820 β ] ( s : Multiset α ) { F : Type _ : Type (?u.39826+1)} [ MonoidHomClass F α β ] ( f : F ) :
( s . map f ). prod = f s . prod :=
Quotient.inductionOn s fun l => by simp only [ l . prod_hom f , quot_mk_to_coe , coe_map , coe_prod ]
#align multiset.prod_hom Multiset.prod_hom
#align multiset.sum_hom Multiset.sum_hom
@[ to_additive ]
theorem prod_hom' [ CommMonoid : Type ?u.42650 → Type ?u.42650 β ] ( s : Multiset ι ) { F : Type _ : Type (?u.42656+1)} [ MonoidHomClass F α β ] ( f : F )
( g : ι → α ) : ( s . map fun i => f <| g i ). prod = f ( s . map g ). prod := by
convert ( s . map g ). prod_hom f
exact ( map_map _ _ _ ). symm : ∀ {α : Sort ?u.47998} {a b : α }, a = b b = a symm
#align multiset.prod_hom' Multiset.prod_hom'
#align multiset.sum_hom' Multiset.sum_hom'
@[ to_additive ]
theorem prod_hom₂ [ CommMonoid : Type ?u.48185 → Type ?u.48185 β ] [ CommMonoid : Type ?u.48188 → Type ?u.48188 γ ] ( s : Multiset ι ) ( f : α → β → γ )
( hf : ∀ (a b : α ) (c d : β ), f (a * b c * d = f a c * f b d hf : ∀ a b c d , f ( a * b ) ( c * d ) = f a c * f b d ) ( hf' : f 1 1 = 1 ) ( f₁ : ι → α )
( f₂ : ι → β ) : ( s . map fun i => f ( f₁ i ) ( f₂ i )). prod = f ( s . map f₁ ). prod ( s . map f₂ ). prod :=
Quotient.inductionOn s fun l => by
simp only [ l . prod_hom₂ f hf : ∀ (a b : α ) (c d : β ), f (a * b c * d = f a c * f b d hf hf' , quot_mk_to_coe , coe_map , coe_prod ]
#align multiset.prod_hom₂ Multiset.prod_hom₂
#align multiset.sum_hom₂ Multiset.sum_hom₂
@[ to_additive ]
theorem prod_hom_rel [ CommMonoid : Type ?u.53544 → Type ?u.53544 β ] ( s : Multiset ι ) { r : α → β → Prop } { f : ι → α } { g : ι → β }
( h₁ : r 1 1 ) ( h₂ : ∀ ⦃a : ι ⦄ ⦃b : α ⦄ ⦃c : β ⦄, r b c r (f a * b g a * c h₂ : ∀ ⦃ a b c ⦄, r b c → r ( f a * b ) ( g a * c )) :
r ( s . map f ). prod ( s . map g ). prod :=
Quotient.inductionOn s fun l => by
simp only [ l . prod_hom_rel h₁ h₂ : ∀ ⦃a : ι ⦄ ⦃b : α ⦄ ⦃c : β ⦄, r b c r (f a * b g a * c h₂ , quot_mk_to_coe , coe_map , coe_prod ]
#align multiset.prod_hom_rel Multiset.prod_hom_rel
#align multiset.sum_hom_rel Multiset.sum_hom_rel
@[ to_additive ]
theorem prod_map_one : prod (map (fun x => 1 ) m = 1 prod_map_one : prod ( m . map fun _ => ( 1 : α )) = 1 := by
rw [ map_const' , prod_replicate , one_pow : ∀ {M : Type ?u.57714} [inst : Monoid M n : ℕ ), 1 ^ n = 1 ]
#align multiset.prod_map_one Multiset.prod_map_one
#align multiset.sum_map_zero Multiset.sum_map_zero
@[ to_additive ( attr := simp )]
theorem prod_map_mul : ( m . map fun i => f i * g i ). prod = ( m . map f ). prod * ( m . map g ). prod :=
m . prod_hom₂ (· * ·) mul_mul_mul_comm ( mul_one _ ) _ _
#align multiset.prod_map_mul Multiset.prod_map_mul
#align multiset.sum_map_add Multiset.sum_map_add
@[ simp ]
theorem prod_map_neg [ HasDistribNeg : (α : Type ?u.63367) → [inst : Mul α Type ?u.63367 α ] ( s : Multiset α ) :
( s . map Neg.neg : {α : Type ?u.63825} → [self : Neg α α → α ). prod = (- 1 ) ^ card s * s . prod :=
Quotient.inductionOn s ( by simp )
#align multiset.prod_map_neg Multiset.prod_map_neg
@[ to_additive ]
theorem prod_map_pow { n : ℕ } : ( m . map fun i => f i ^ n ). prod = ( m . map f ). prod ^ n :=
m . prod_hom' ( powMonoidHom n : α →* α ) f
#align multiset.prod_map_pow Multiset.prod_map_pow
#align multiset.sum_map_nsmul Multiset.sum_map_nsmul
@[ to_additive ]
theorem prod_map_prod_map ( m : Multiset β ) ( n : Multiset γ ) { f : β → γ → α } :
prod ( m . map fun a => prod <| n . map fun b => f a b ) =
prod ( n . map fun b => prod <| m . map fun a => f a b ) :=
Multiset.induction_on m ( by simp ) fun a m ih => by simp [ ih ]
#align multiset.prod_map_prod_map Multiset.prod_map_prod_map
#align multiset.sum_map_sum_map Multiset.sum_map_sum_map
@[ to_additive ]
theorem prod_induction : ∀ {α : Type u_1} [inst : CommMonoid α p : α → Prop s : Multiset α (∀ (a b : α ), p a p b p (a * b ) → p 1 (∀ (a : α ), a ∈ s p a ) → p (prod s prod_induction ( p : α → Prop ) ( s : Multiset α ) ( p_mul : ∀ (a b : α ), p a p b p (a * b p_mul : ∀ a b , p a → p b → p ( a * b ))
( p_one : p 1 ) ( p_s : ∀ (a : α ), a ∈ s p a p_s : ∀ a ∈ s , p a ) : p s . prod := by
rw [ prod_eq_foldr p (foldr (fun x x_1 => x * x_1 ) (_ : ∀ (x y z : α ), x * (y * z = y * (x * z ) 1 s ] p (foldr (fun x x_1 => x * x_1 ) (_ : ∀ (x y z : α ), x * (y * z = y * (x * z ) 1 s
exact foldr_induction : ∀ {α : Type ?u.81034} (f : α → α → α H : LeftCommutative f x : α ) (p : α → Prop s : Multiset α (∀ (a b : α ), p a p b p (f a b ) → p x (∀ (a : α ), a ∈ s p a ) → p (foldr f H x s (· * ·) ( fun x y z => p (foldr (fun x x_1 => x * x_1 ) (_ : ∀ (x y z : α ), x * (y * z = y * (x * z ) 1 s by (fun x x_1 => x * x_1 ) x ((fun x x_1 => x * x_1 ) y z ) = (fun x x_1 => x * x_1 ) y ((fun x x_1 => x * x_1 ) x z ) simp [ mul_left_comm ] ) 1 p s p_mul : ∀ (a b : α ), p a p b p (a * b p_mul p_one p_s : ∀ (a : α ), a ∈ s p a p_s
#align multiset.prod_induction Multiset.prod_induction : ∀ {α : Type u_1} [inst : CommMonoid α p : α → Prop s : Multiset α (∀ (a b : α ), p a p b p (a * b ) → p 1 (∀ (a : α ), a ∈ s p a ) → p (prod s
#align multiset.sum_induction Multiset.sum_induction : ∀ {α : Type u_1} [inst : AddCommMonoid α p : α → Prop s : Multiset α (∀ (a b : α ), p a p b p (a + b ) → p 0 (∀ (a : α ), a ∈ s p a ) → p (sum s
@[ to_additive ]
theorem prod_induction_nonempty : ∀ {α : Type u_1} [inst : CommMonoid α s : Multiset α p : α → Prop (∀ (a b : α ), p a p b p (a * b ) → s ≠ ∅ (∀ (a : α ), a ∈ s p a ) → p (prod s prod_induction_nonempty ( p : α → Prop ) ( p_mul : ∀ (a b : α ), p a p b p (a * b p_mul : ∀ a b , p a → p b → p ( a * b )) ( hs : s ≠ ∅ )
( p_s : ∀ (a : α ), a ∈ s p a p_s : ∀ a ∈ s , p a ) : p s . prod := by
-- Porting note: used `refine' Multiset.induction _ _`
induction' s using Multiset.induction_on with a s hsa