Documentation

Mathlib.Data.Fintype.BigOperators

Results about "big operations" over a Fintype, and consequent results about cardinalities of certain types.

Implementation note #

This content had previously been in Data.Fintype.Basic, but was moved here to avoid requiring Algebra.BigOperators (and hence many other imports) as a dependency of Fintype.

However many of the results here really belong in Algebra.BigOperators.Group.Finset and should be moved at some point.

theorem Fintype.sum_bool {α : Type u_1} [AddCommMonoid α] (f : Boolα) :
b : Bool, f b = f true + f false
theorem Fintype.prod_bool {α : Type u_1} [CommMonoid α] (f : Boolα) :
b : Bool, f b = f true * f false
theorem Fintype.card_eq_sum_ones {α : Type u_4} [Fintype α] :
Fintype.card α = _a : α, 1
theorem Fintype.sum_extend_by_zero {α : Type u_1} {ι : Type u_4} [DecidableEq ι] [Fintype ι] [AddCommMonoid α] (s : Finset ι) (f : ια) :
(∑ i : ι, if i s then f i else 0) = is, f i
theorem Fintype.prod_extend_by_one {α : Type u_1} {ι : Type u_4} [DecidableEq ι] [Fintype ι] [CommMonoid α] (s : Finset ι) (f : ια) :
(∏ i : ι, if i s then f i else 1) = is, f i
theorem Fintype.sum_eq_zero {α : Type u_1} {M : Type u_4} [Fintype α] [AddCommMonoid M] (f : αM) (h : ∀ (a : α), f a = 0) :
a : α, f a = 0
theorem Fintype.prod_eq_one {α : Type u_1} {M : Type u_4} [Fintype α] [CommMonoid M] (f : αM) (h : ∀ (a : α), f a = 1) :
a : α, f a = 1
theorem Fintype.sum_congr {α : Type u_1} {M : Type u_4} [Fintype α] [AddCommMonoid M] (f : αM) (g : αM) (h : ∀ (a : α), f a = g a) :
a : α, f a = a : α, g a
theorem Fintype.prod_congr {α : Type u_1} {M : Type u_4} [Fintype α] [CommMonoid M] (f : αM) (g : αM) (h : ∀ (a : α), f a = g a) :
a : α, f a = a : α, g a
theorem Fintype.sum_eq_single {α : Type u_1} {M : Type u_4} [Fintype α] [AddCommMonoid M] {f : αM} (a : α) (h : ∀ (x : α), x af x = 0) :
x : α, f x = f a
theorem Fintype.prod_eq_single {α : Type u_1} {M : Type u_4} [Fintype α] [CommMonoid M] {f : αM} (a : α) (h : ∀ (x : α), x af x = 1) :
x : α, f x = f a
theorem Fintype.sum_eq_add {α : Type u_1} {M : Type u_4} [Fintype α] [AddCommMonoid M] {f : αM} (a : α) (b : α) (h₁ : a b) (h₂ : ∀ (x : α), x a x bf x = 0) :
x : α, f x = f a + f b
theorem Fintype.prod_eq_mul {α : Type u_1} {M : Type u_4} [Fintype α] [CommMonoid M] {f : αM} (a : α) (b : α) (h₁ : a b) (h₂ : ∀ (x : α), x a x bf x = 1) :
x : α, f x = f a * f b
theorem Fintype.eq_of_subsingleton_of_sum_eq {M : Type u_4} [AddCommMonoid M] {ι : Type u_5} [Subsingleton ι] {s : Finset ι} {f : ιM} {b : M} (h : is, f i = b) (i : ι) :
i sf i = b

If a sum of a Finset of a subsingleton type has a given value, so do the terms in that sum.

theorem Fintype.eq_of_subsingleton_of_prod_eq {M : Type u_4} [CommMonoid M] {ι : Type u_5} [Subsingleton ι] {s : Finset ι} {f : ιM} {b : M} (h : is, f i = b) (i : ι) :
i sf i = b

If a product of a Finset of a subsingleton type has a given value, so do the terms in that product.

@[simp]
theorem Fintype.sum_option {α : Type u_1} {M : Type u_4} [Fintype α] [AddCommMonoid M] (f : Option αM) :
i : Option α, f i = f none + i : α, f (some i)
@[simp]
theorem Fintype.prod_option {α : Type u_1} {M : Type u_4} [Fintype α] [CommMonoid M] (f : Option αM) :
i : Option α, f i = f none * i : α, f (some i)
@[simp]
theorem Finset.card_pi {ι : Type u_4} {α : ιType u_6} [DecidableEq ι] (s : Finset ι) (t : (i : ι) → Finset (α i)) :
(s.pi t).card = is, (t i).card
@[simp]
theorem Fintype.card_piFinset {ι : Type u_4} {α : ιType u_6} [DecidableEq ι] [Fintype ι] (s : (i : ι) → Finset (α i)) :
(Fintype.piFinset s).card = i : ι, (s i).card
theorem Fintype.card_piFinset_const {α : Type u_7} (s : Finset α) (n : ) :
(Fintype.piFinset fun (x : Fin n) => s).card = s.card ^ n

This lemma is specifically designed to be used backwards, whence the specialisation to Fin n as the indexing type doesn't matter in practice. The more general forward direction lemma here is Fintype.card_piFinset.

@[simp]
theorem Fintype.card_pi {ι : Type u_4} {α : ιType u_6} [DecidableEq ι] [Fintype ι] [(i : ι) → Fintype (α i)] :
Fintype.card ((i : ι) → α i) = i : ι, Fintype.card (α i)
theorem Fintype.card_pi_const (α : Type u_7) [Fintype α] (n : ) :
Fintype.card (Fin nα) = Fintype.card α ^ n

This lemma is specifically designed to be used backwards, whence the specialisation to Fin n as the indexing type doesn't matter in practice. The more general forward direction lemma here is Fintype.card_pi.

@[simp]
theorem Fintype.card_sigma {ι : Type u_8} {α : ιType u_7} [Fintype ι] [(i : ι) → Fintype (α i)] :
Fintype.card (Sigma α) = i : ι, Fintype.card (α i)
theorem Fintype.card_filter_piFinset_eq_of_mem {ι : Type u_4} {α : ιType u_6} [DecidableEq ι] [Fintype ι] [(i : ι) → DecidableEq (α i)] (s : (i : ι) → Finset (α i)) (i : ι) {a : α i} (ha : a s i) :
(Finset.filter (fun (f : (a : ι) → α a) => f i = a) (Fintype.piFinset s)).card = jFinset.univ.erase i, (s j).card

The number of dependent maps f : Π j, s j for which the i component is a is the product over all j ≠ i of (s j).card.

Note that this is just a composition of easier lemmas, but there's some glue missing to make that smooth enough not to need this lemma.

theorem Fintype.card_filter_piFinset_const_eq_of_mem {ι : Type u_4} {κ : Type u_5} [DecidableEq ι] [DecidableEq κ] [Fintype ι] (s : Finset κ) (i : ι) {x : κ} (hx : x s) :
(Finset.filter (fun (f : ικ) => f i = x) (Fintype.piFinset fun (x : ι) => s)).card = s.card ^ (Fintype.card ι - 1)
theorem Fintype.card_filter_piFinset_eq {ι : Type u_4} {α : ιType u_6} [DecidableEq ι] [Fintype ι] [(i : ι) → DecidableEq (α i)] (s : (i : ι) → Finset (α i)) (i : ι) (a : α i) :
(Finset.filter (fun (f : (a : ι) → α a) => f i = a) (Fintype.piFinset s)).card = if a s i then bFinset.univ.erase i, (s b).card else 0
theorem Fintype.card_filter_piFinset_const {ι : Type u_4} {κ : Type u_5} [DecidableEq ι] [DecidableEq κ] [Fintype ι] (s : Finset κ) (i : ι) (j : κ) :
(Finset.filter (fun (f : ικ) => f i = j) (Fintype.piFinset fun (x : ι) => s)).card = if j s then s.card ^ (Fintype.card ι - 1) else 0
theorem Fintype.card_fun {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] :
@[simp]
theorem card_vector {α : Type u_1} [Fintype α] (n : ) :
theorem Fin.sum_univ_eq_sum_range {α : Type u_1} [AddCommMonoid α] (f : α) (n : ) :
i : Fin n, f i = iFinset.range n, f i

It is equivalent to sum a function over fin n or finset.range n.

theorem Fin.prod_univ_eq_prod_range {α : Type u_1} [CommMonoid α] (f : α) (n : ) :
i : Fin n, f i = iFinset.range n, f i

It is equivalent to compute the product of a function over Fin n or Finset.range n.

theorem Finset.sum_fin_eq_sum_range {β : Type u_2} [AddCommMonoid β] {n : } (c : Fin nβ) :
i : Fin n, c i = iFinset.range n, if h : i < n then c i, h else 0
theorem Finset.prod_fin_eq_prod_range {β : Type u_2} [CommMonoid β] {n : } (c : Fin nβ) :
i : Fin n, c i = iFinset.range n, if h : i < n then c i, h else 1
theorem Finset.sum_toFinset_eq_subtype {α : Type u_1} {M : Type u_4} [AddCommMonoid M] [Fintype α] (p : αProp) [DecidablePred p] (f : αM) :
a{x : α | p x}.toFinset, f a = a : Subtype p, f a
theorem Finset.prod_toFinset_eq_subtype {α : Type u_1} {M : Type u_4} [CommMonoid M] [Fintype α] (p : αProp) [DecidablePred p] (f : αM) :
a{x : α | p x}.toFinset, f a = a : Subtype p, f a
theorem Fintype.prod_dite {α : Type u_1} {β : Type u_2} [Fintype α] {p : αProp} [DecidablePred p] [CommMonoid β] (f : (a : α) → p aβ) (g : (a : α) → ¬p aβ) :
a : α, dite (p a) (f a) (g a) = (∏ a : { a : α // p a }, f a ) * a : { a : α // ¬p a }, g a
theorem Fintype.sum_sum_elim {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [Fintype α₁] [Fintype α₂] [AddCommMonoid M] (f : α₁M) (g : α₂M) :
x : α₁ α₂, Sum.elim f g x = a₁ : α₁, f a₁ + a₂ : α₂, g a₂
theorem Fintype.prod_sum_elim {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [Fintype α₁] [Fintype α₂] [CommMonoid M] (f : α₁M) (g : α₂M) :
x : α₁ α₂, Sum.elim f g x = (∏ a₁ : α₁, f a₁) * a₂ : α₂, g a₂
@[simp]
theorem Fintype.sum_sum_type {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [Fintype α₁] [Fintype α₂] [AddCommMonoid M] (f : α₁ α₂M) :
x : α₁ α₂, f x = a₁ : α₁, f (Sum.inl a₁) + a₂ : α₂, f (Sum.inr a₂)
@[simp]
theorem Fintype.prod_sum_type {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [Fintype α₁] [Fintype α₂] [CommMonoid M] (f : α₁ α₂M) :
x : α₁ α₂, f x = (∏ a₁ : α₁, f (Sum.inl a₁)) * a₂ : α₂, f (Sum.inr a₂)
@[simp]
theorem Fintype.sum_prod_type {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [AddCommMonoid γ] {f : α₁ × α₂γ} :
x : α₁ × α₂, f x = x : α₁, y : α₂, f (x, y)
@[simp]
theorem Fintype.prod_prod_type {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [CommMonoid γ] {f : α₁ × α₂γ} :
x : α₁ × α₂, f x = x : α₁, y : α₂, f (x, y)
theorem Fintype.sum_prod_type' {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [AddCommMonoid γ] {f : α₁α₂γ} :
x : α₁ × α₂, f x.1 x.2 = x : α₁, y : α₂, f x y

An uncurried version of Finset.sum_prod_type

theorem Fintype.prod_prod_type' {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [CommMonoid γ] {f : α₁α₂γ} :
x : α₁ × α₂, f x.1 x.2 = x : α₁, y : α₂, f x y

An uncurried version of Finset.prod_prod_type.

theorem Fintype.sum_prod_type_right {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [AddCommMonoid γ] {f : α₁ × α₂γ} :
x : α₁ × α₂, f x = y : α₂, x : α₁, f (x, y)
theorem Fintype.prod_prod_type_right {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [CommMonoid γ] {f : α₁ × α₂γ} :
x : α₁ × α₂, f x = y : α₂, x : α₁, f (x, y)
theorem Fintype.sum_prod_type_right' {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [AddCommMonoid γ] {f : α₁α₂γ} :
x : α₁ × α₂, f x.1 x.2 = y : α₂, x : α₁, f x y

An uncurried version of Finset.sum_prod_type_right

theorem Fintype.prod_prod_type_right' {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [CommMonoid γ] {f : α₁α₂γ} :
x : α₁ × α₂, f x.1 x.2 = y : α₂, x : α₁, f x y

An uncurried version of Finset.prod_prod_type_right.