mathlib3 documentation

algebra.big_operators.fin

Big operators and fin #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Some results about products and sums over the type fin.

The most important results are the induction formulas fin.prod_univ_cast_succ and fin.prod_univ_succ, and the formula fin.prod_const for the product of a constant function. These results have variants for sums instead of products.

Main declarations #

source
theorem finset.sum_range {β : Type u_2} [add_comm_monoid β] {n : ℕ} (f : ℕ → β) :
(finset.range n).sum (λ (i : ℕ), f i) = finset.univ.sum (λ (i : fin n), f ↑i)
source
theorem finset.prod_range {β : Type u_2} [comm_monoid β] {n : ℕ} (f : ℕ → β) :
(finset.range n).prod (λ (i : ℕ), f i) = finset.univ.prod (λ (i : fin n), f ↑i)
source
theorem fin.prod_univ_def {β : Type u_2} [comm_monoid β] {n : ℕ} (f : fin n → β) :
finset.univ.prod (λ (i : fin n), f i) = (list.map f (list.fin_range n)).prod
source
theorem fin.sum_univ_def {β : Type u_2} [add_comm_monoid β] {n : ℕ} (f : fin n → β) :
finset.univ.sum (λ (i : fin n), f i) = (list.map f (list.fin_range n)).sum
source
theorem fin.sum_of_fn {β : Type u_2} [add_comm_monoid β] {n : ℕ} (f : fin n → β) :
(list.of_fn f).sum = finset.univ.sum (λ (i : fin n), f i)
source
theorem fin.prod_of_fn {β : Type u_2} [comm_monoid β] {n : ℕ} (f : fin n → β) :
(list.of_fn f).prod = finset.univ.prod (λ (i : fin n), f i)
source
theorem fin.sum_univ_zero {β : Type u_2} [add_comm_monoid β] (f : fin 0 → β) :
finset.univ.sum (λ (i : fin 0), f i) = 0

A sum of a function f : fin 0 → β is 0 because fin 0 is empty

source
theorem fin.prod_univ_zero {β : Type u_2} [comm_monoid β] (f : fin 0 → β) :
finset.univ.prod (λ (i : fin 0), f i) = 1

A product of a function f : fin 0 → β is 1 because fin 0 is empty

source
theorem fin.prod_univ_succ_above {β : Type u_2} [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) (x : fin (n + 1)) :
finset.univ.prod (λ (i : fin (n + 1)), f i) = f x * finset.univ.prod (λ (i : fin n), f (⇑(x.succ_above) i))

A product of a function f : fin (n + 1) → β over all fin (n + 1) is the product of f x, for some x : fin (n + 1) times the remaining product

source
theorem fin.sum_univ_succ_above {β : Type u_2} [add_comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) (x : fin (n + 1)) :
finset.univ.sum (λ (i : fin (n + 1)), f i) = f x + finset.univ.sum (λ (i : fin n), f (⇑(x.succ_above) i))

A sum of a function f : fin (n + 1) → β over all fin (n + 1) is the sum of f x, for some x : fin (n + 1) plus the remaining product

source
theorem fin.prod_univ_succ {β : Type u_2} [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) :
finset.univ.prod (λ (i : fin (n + 1)), f i) = f 0 * finset.univ.prod (λ (i : fin n), f i.succ)

A product of a function f : fin (n + 1) → β over all fin (n + 1) is the product of f 0 plus the remaining product

source
theorem fin.sum_univ_succ {β : Type u_2} [add_comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) :
finset.univ.sum (λ (i : fin (n + 1)), f i) = f 0 + finset.univ.sum (λ (i : fin n), f i.succ)

A sum of a function f : fin (n + 1) → β over all fin (n + 1) is the sum of f 0 plus the remaining product

source
theorem fin.sum_univ_cast_succ {β : Type u_2} [add_comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) :
finset.univ.sum (λ (i : fin (n + 1)), f i) = finset.univ.sum (λ (i : fin n), f (⇑fin.cast_succ i)) + f (fin.last n)

A sum of a function f : fin (n + 1) → β over all fin (n + 1) is the sum of f (fin.last n) plus the remaining sum

source
theorem fin.prod_univ_cast_succ {β : Type u_2} [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) :
finset.univ.prod (λ (i : fin (n + 1)), f i) = finset.univ.prod (λ (i : fin n), f (⇑fin.cast_succ i)) * f (fin.last n)

A product of a function f : fin (n + 1) → β over all fin (n + 1) is the product of f (fin.last n) plus the remaining product

source
theorem fin.sum_cons {β : Type u_2} [add_comm_monoid β] {n : ℕ} (x : β) (f : fin n → β) :
finset.univ.sum (λ (i : fin n.succ), fin.cons x f i) = x + finset.univ.sum (λ (i : fin n), f i)
source
theorem fin.prod_cons {β : Type u_2} [comm_monoid β] {n : ℕ} (x : β) (f : fin n → β) :
finset.univ.prod (λ (i : fin n.succ), fin.cons x f i) = x * finset.univ.prod (λ (i : fin n), f i)
source
theorem fin.prod_univ_one {β : Type u_2} [comm_monoid β] (f : fin 1 → β) :
finset.univ.prod (λ (i : fin 1), f i) = f 0
source
theorem fin.sum_univ_one {β : Type u_2} [add_comm_monoid β] (f : fin 1 → β) :
finset.univ.sum (λ (i : fin 1), f i) = f 0
source
@[simp]
theorem fin.prod_univ_two {β : Type u_2} [comm_monoid β] (f : fin 2 → β) :
finset.univ.prod (λ (i : fin 2), f i) = f 0 * f 1
source
@[simp]
theorem fin.sum_univ_two {β : Type u_2} [add_comm_monoid β] (f : fin 2 → β) :
finset.univ.sum (λ (i : fin 2), f i) = f 0 + f 1
source
theorem fin.sum_univ_three {β : Type u_2} [add_comm_monoid β] (f : fin 3 → β) :
finset.univ.sum (λ (i : fin 3), f i) = f 0 + f 1 + f 2
source
theorem fin.prod_univ_three {β : Type u_2} [comm_monoid β] (f : fin 3 → β) :
finset.univ.prod (λ (i : fin 3), f i) = f 0 * f 1 * f 2
source
theorem fin.prod_univ_four {β : Type u_2} [comm_monoid β] (f : fin 4 → β) :
finset.univ.prod (λ (i : fin 4), f i) = f 0 * f 1 * f 2 * f 3
source
theorem fin.sum_univ_four {β : Type u_2} [add_comm_monoid β] (f : fin 4 → β) :
finset.univ.sum (λ (i : fin 4), f i) = f 0 + f 1 + f 2 + f 3
source
theorem fin.sum_univ_five {β : Type u_2} [add_comm_monoid β] (f : fin 5 → β) :
finset.univ.sum (λ (i : fin 5), f i) = f 0 + f 1 + f 2 + f 3 + f 4
source
theorem fin.prod_univ_five {β : Type u_2} [comm_monoid β] (f : fin 5 → β) :
finset.univ.prod (λ (i : fin 5), f i) = f 0 * f 1 * f 2 * f 3 * f 4
source
theorem fin.sum_univ_six {β : Type u_2} [add_comm_monoid β] (f : fin 6 → β) :
finset.univ.sum (λ (i : fin 6), f i) = f 0 + f 1 + f 2 + f 3 + f 4 + f 5
source
theorem fin.prod_univ_six {β : Type u_2} [comm_monoid β] (f : fin 6 → β) :
finset.univ.prod (λ (i : fin 6), f i) = f 0 * f 1 * f 2 * f 3 * f 4 * f 5
source
theorem fin.prod_univ_seven {β : Type u_2} [comm_monoid β] (f : fin 7 → β) :
finset.univ.prod (λ (i : fin 7), f i) = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6
source
theorem fin.sum_univ_seven {β : Type u_2} [add_comm_monoid β] (f : fin 7 → β) :
finset.univ.sum (λ (i : fin 7), f i) = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6
source
theorem fin.sum_univ_eight {β : Type u_2} [add_comm_monoid β] (f : fin 8 → β) :
finset.univ.sum (λ (i : fin 8), f i) = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6 + f 7
source
theorem fin.prod_univ_eight {β : Type u_2} [comm_monoid β] (f : fin 8 → β) :
finset.univ.prod (λ (i : fin 8), f i) = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7
source
theorem fin.sum_pow_mul_eq_add_pow {n : ℕ} {R : Type u_1} [comm_semiring R] (a b : R) :
finset.univ.sum (λ (s : finset (fin n)), a ^ s.card * b ^ (n - s.card)) = (a + b) ^ n
source
theorem fin.prod_const {α : Type u_1} [comm_monoid α] (n : ℕ) (x : α) :
finset.univ.prod (λ (i : fin n), x) = x ^ n
source
theorem fin.sum_const {α : Type u_1} [add_comm_monoid α] (n : ℕ) (x : α) :
finset.univ.sum (λ (i : fin n), x) = n • x
source
theorem fin.sum_Ioi_zero {M : Type u_1} [add_comm_monoid M] {n : ℕ} {v : fin n.succ → M} :
(finset.Ioi 0).sum (λ (i : fin n.succ), v i) = finset.univ.sum (λ (j : fin n), v j.succ)
source
theorem fin.prod_Ioi_zero {M : Type u_1} [comm_monoid M] {n : ℕ} {v : fin n.succ → M} :
(finset.Ioi 0).prod (λ (i : fin n.succ), v i) = finset.univ.prod (λ (j : fin n), v j.succ)
source
theorem fin.sum_Ioi_succ {M : Type u_1} [add_comm_monoid M] {n : ℕ} (i : fin n) (v : fin n.succ → M) :
(finset.Ioi i.succ).sum (λ (j : fin n.succ), v j) = (finset.Ioi i).sum (λ (j : fin n), v j.succ)
source
theorem fin.prod_Ioi_succ {M : Type u_1} [comm_monoid M] {n : ℕ} (i : fin n) (v : fin n.succ → M) :
(finset.Ioi i.succ).prod (λ (j : fin n.succ), v j) = (finset.Ioi i).prod (λ (j : fin n), v j.succ)
source
theorem fin.sum_congr' {M : Type u_1} [add_comm_monoid M] {a b : ℕ} (f : fin b → M) (h : a = b) :
finset.univ.sum (λ (i : fin a), f (⇑(fin.cast h) i)) = finset.univ.sum (λ (i : fin b), f i)
source
theorem fin.prod_congr' {M : Type u_1} [comm_monoid M] {a b : ℕ} (f : fin b → M) (h : a = b) :
finset.univ.prod (λ (i : fin a), f (⇑(fin.cast h) i)) = finset.univ.prod (λ (i : fin b), f i)
source
theorem fin.prod_univ_add {M : Type u_1} [comm_monoid M] {a b : ℕ} (f : fin (a + b) → M) :
finset.univ.prod (λ (i : fin (a + b)), f i) = finset.univ.prod (λ (i : fin a), f (⇑(fin.cast_add b) i)) * finset.univ.prod (λ (i : fin b), f (⇑(fin.nat_add a) i))
source
theorem fin.sum_univ_add {M : Type u_1} [add_comm_monoid M] {a b : ℕ} (f : fin (a + b) → M) :
finset.univ.sum (λ (i : fin (a + b)), f i) = finset.univ.sum (λ (i : fin a), f (⇑(fin.cast_add b) i)) + finset.univ.sum (λ (i : fin b), f (⇑(fin.nat_add a) i))
source
theorem fin.prod_trunc {M : Type u_1} [comm_monoid M] {a b : ℕ} (f : fin (a + b) → M) (hf : ∀ (j : fin b), f (⇑(fin.nat_add a) j) = 1) :
finset.univ.prod (λ (i : fin (a + b)), f i) = finset.univ.prod (λ (i : fin a), f (⇑(fin.cast_le _) i))
source
theorem fin.sum_trunc {M : Type u_1} [add_comm_monoid M] {a b : ℕ} (f : fin (a + b) → M) (hf : ∀ (j : fin b), f (⇑(fin.nat_add a) j) = 0) :
finset.univ.sum (λ (i : fin (a + b)), f i) = finset.univ.sum (λ (i : fin a), f (⇑(fin.cast_le _) i))
source
def fin.partial_prod {α : Type u_1} [monoid α] {n : ℕ} (f : fin n → α) (i : fin (n + 1)) :
α

For f = (a₁, ..., aₙ) in αⁿ, partial_prod f is (1, a₁, a₁a₂, ..., a₁...aₙ) in αⁿ⁺¹.

Equations
source
def fin.partial_sum {α : Type u_1} [add_monoid α] {n : ℕ} (f : fin n → α) (i : fin (n + 1)) :
α

For f = (a₁, ..., aₙ) in αⁿ, partial_sum f is (0, a₁, a₁ + a₂, ..., a₁ + ... + aₙ) in αⁿ⁺¹.

Equations
source
@[simp]
theorem fin.partial_sum_zero {α : Type u_1} [add_monoid α] {n : ℕ} (f : fin n → α) :
fin.partial_sum f 0 = 0
source
@[simp]
theorem fin.partial_prod_zero {α : Type u_1} [monoid α] {n : ℕ} (f : fin n → α) :
fin.partial_prod f 0 = 1
source
theorem fin.partial_sum_succ {α : Type u_1} [add_monoid α] {n : ℕ} (f : fin n → α) (j : fin n) :
fin.partial_sum f j.succ = fin.partial_sum f (⇑fin.cast_succ j) + f j
source
theorem fin.partial_prod_succ {α : Type u_1} [monoid α] {n : ℕ} (f : fin n → α) (j : fin n) :
fin.partial_prod f j.succ = fin.partial_prod f (⇑fin.cast_succ j) * f j
source
theorem fin.partial_prod_succ' {α : Type u_1} [monoid α] {n : ℕ} (f : fin (n + 1) → α) (j : fin (n + 1)) :
fin.partial_prod f j.succ = f 0 * fin.partial_prod (fin.tail f) j
source
theorem fin.partial_sum_succ' {α : Type u_1} [add_monoid α] {n : ℕ} (f : fin (n + 1) → α) (j : fin (n + 1)) :
fin.partial_sum f j.succ = f 0 + fin.partial_sum (fin.tail f) j
source
theorem fin.partial_sum_left_neg {n : ℕ} {G : Type u_1} [add_group G] (f : fin (n + 1) → G) :
f 0 +ᵥ fin.partial_sum (λ (i : fin n), -f ↑i + f i.succ) = f
source
theorem fin.partial_prod_left_inv {n : ℕ} {G : Type u_1} [group G] (f : fin (n + 1) → G) :
f 0 • fin.partial_prod (λ (i : fin n), (f ↑i)⁻¹ * f i.succ) = f
source
theorem fin.partial_prod_right_inv {n : ℕ} {G : Type u_1} [group G] (f : fin n → G) (i : fin n) :
(fin.partial_prod f (⇑fin.cast_succ i))⁻¹ * fin.partial_prod f i.succ = f i
source
theorem fin.partial_sum_right_neg {n : ℕ} {G : Type u_1} [add_group G] (f : fin n → G) (i : fin n) :
-fin.partial_sum f (⇑fin.cast_succ i) + fin.partial_sum f i.succ = f i
source
theorem fin.neg_partial_sum_add_eq_contract_nth {n : ℕ} {G : Type u_1} [add_group G] (g : fin (n + 1) → G) (j : fin (n + 1)) (k : fin n) :
-fin.partial_sum g (⇑(j.succ.succ_above) (⇑fin.cast_succ k)) + fin.partial_sum g (⇑(j.succ_above) k).succ = j.contract_nth has_add.add g k

Let (g₀, g₁, ..., gₙ) be a tuple of elements in Gⁿ⁺¹. Then if k < j, this says -(g₀ + g₁ + ... + gₖ₋₁) + (g₀ + g₁ + ... + gₖ) = gₖ. If k = j, it says -(g₀ + g₁ + ... + gₖ₋₁) + (g₀ + g₁ + ... + gₖ₊₁) = gₖ + gₖ₊₁. If k > j, it says -(g₀ + g₁ + ... + gₖ) + (g₀ + g₁ + ... + gₖ₊₁) = gₖ₊₁. Useful for defining group cohomology.

source
theorem fin.inv_partial_prod_mul_eq_contract_nth {n : ℕ} {G : Type u_1} [group G] (g : fin (n + 1) → G) (j : fin (n + 1)) (k : fin n) :
(fin.partial_prod g (⇑(j.succ.succ_above) (⇑fin.cast_succ k)))⁻¹ * fin.partial_prod g (⇑(j.succ_above) k).succ = j.contract_nth has_mul.mul g k

Let (g₀, g₁, ..., gₙ) be a tuple of elements in Gⁿ⁺¹. Then if k < j, this says (g₀g₁...gₖ₋₁)⁻¹ * g₀g₁...gₖ = gₖ. If k = j, it says (g₀g₁...gₖ₋₁)⁻¹ * g₀g₁...gₖ₊₁ = gₖgₖ₊₁. If k > j, it says (g₀g₁...gₖ)⁻¹ * g₀g₁...gₖ₊₁ = gₖ₊₁. Useful for defining group cohomology.

source
@[simp]
theorem fin_function_fin_equiv_symm_apply_val {m n : ℕ} (a : fin (m ^ n)) (b : fin n) :
(⇑(fin_function_fin_equiv.symm) a b).val = ↑a / m ^ ↑b % m
source
def fin_function_fin_equiv {m n : ℕ} :
(fin n → fin m) ≃ fin (m ^ n)

Equivalence between fin n → fin m and fin (m ^ n).

Equations
source
@[simp]
theorem fin_function_fin_equiv_apply_val {m n : ℕ} (f : fin n → fin m) :
(⇑fin_function_fin_equiv f).val = finset.univ.sum (λ (i : fin n), ↑(f i) * m ^ ↑i)
source
theorem fin_function_fin_equiv_apply {m n : ℕ} (f : fin n → fin m) :
↑(⇑fin_function_fin_equiv f) = finset.univ.sum (λ (i : fin n), ↑(f i) * m ^ ↑i)
source
theorem fin_function_fin_equiv_single {m n : ℕ} [ne_zero m] (i : fin n) (j : fin m) :
↑(⇑fin_function_fin_equiv (pi.single i j)) = ↑j * m ^ ↑i
source
def fin_pi_fin_equiv {m : ℕ} {n : fin m → ℕ} :
(Π (i : fin m), fin (n i)) ≃ fin (finset.univ.prod (λ (i : fin m), n i))

Equivalence between Π i : fin m, fin (n i) and fin (∏ i : fin m, n i).

Equations
source
theorem fin_pi_fin_equiv_apply {m : ℕ} {n : fin m → ℕ} (f : Π (i : fin m), fin (n i)) :
↑(⇑fin_pi_fin_equiv f) = finset.univ.sum (λ (i : fin m), ↑(f i) * finset.univ.prod (λ (j : fin ↑i), n (⇑(fin.cast_le _) j)))
source
theorem fin_pi_fin_equiv_single {m : ℕ} {n : fin m → ℕ} [∀ (i : fin m), ne_zero (n i)] (i : fin m) (j : fin (n i)) :
↑(⇑fin_pi_fin_equiv (pi.single i j)) = ↑j * finset.univ.prod (λ (j : fin ↑i), n (⇑(fin.cast_le _) j))
source
theorem list.sum_take_of_fn {α : Type u_1} [add_comm_monoid α] {n : ℕ} (f : fin n → α) (i : ℕ) :
(list.take i (list.of_fn f)).sum = (finset.filter (λ (j : fin n), j.val < i) finset.univ).sum (λ (j : fin n), f j)
source
theorem list.prod_take_of_fn {α : Type u_1} [comm_monoid α] {n : ℕ} (f : fin n → α) (i : ℕ) :
(list.take i (list.of_fn f)).prod = (finset.filter (λ (j : fin n), j.val < i) finset.univ).prod (λ (j : fin n), f j)
source
theorem list.sum_of_fn {α : Type u_1} [add_comm_monoid α] {n : ℕ} {f : fin n → α} :
(list.of_fn f).sum = finset.univ.sum (λ (i : fin n), f i)
source
theorem list.prod_of_fn {α : Type u_1} [comm_monoid α] {n : ℕ} {f : fin n → α} :
(list.of_fn f).prod = finset.univ.prod (λ (i : fin n), f i)
source
theorem list.alternating_sum_eq_finset_sum {G : Type u_1} [add_comm_group G] (L : list G) :
L.alternating_sum = finset.univ.sum (λ (i : fin L.length), (-1) ^ ↑i • L.nth_le ↑i _)
source
theorem list.alternating_prod_eq_finset_prod {G : Type u_1} [comm_group G] (L : list G) :
L.alternating_prod = finset.univ.prod (λ (i : fin L.length), L.nth_le ↑i _ ^ (-1) ^ ↑i)