Big operators and Fin

Some results about products and sums over the type Fin.

The most important results are the induction formulas Fin.prod_univ_castSucc 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

• finFunctionFinEquiv: An explicit equivalence between Fin n → Fin m and Fin (m ^ n).

theorem Finset.sum_range {β : Type u_2} [AddCommMonoid β] {n : ℕ} (f : ℕ → β) : (Finset.sum (Finset.range n) fun (i : ℕ) => f i) = Finset.sum Finset.univ fun (i : Fin n) => f ↑i

theorem Finset.prod_range {β : Type u_2} [CommMonoid β] {n : ℕ} (f : ℕ → β) : (Finset.prod (Finset.range n) fun (i : ℕ) => f i) = Finset.prod Finset.univ fun (i : Fin n) => f ↑i

theorem Fin.sum_univ_def {β : Type u_2} [AddCommMonoid β] {n : ℕ} (f : Fin n → β) : (Finset.sum Finset.univ fun (i : Fin n) => f i) = List.sum (List.map f (List.finRange n))

theorem Fin.prod_univ_def {β : Type u_2} [CommMonoid β] {n : ℕ} (f : Fin n → β) : (Finset.prod Finset.univ fun (i : Fin n) => f i) = List.prod (List.map f (List.finRange n))

theorem Fin.sum_ofFn {β : Type u_2} [AddCommMonoid β] {n : ℕ} (f : Fin n → β) : List.sum (List.ofFn f) = Finset.sum Finset.univ fun (i : Fin n) => f i

theorem Fin.prod_ofFn {β : Type u_2} [CommMonoid β] {n : ℕ} (f : Fin n → β) : List.prod (List.ofFn f) = Finset.prod Finset.univ fun (i : Fin n) => f i

theorem Fin.sum_univ_zero {β : Type u_2} [AddCommMonoid β] (f : Fin 0 → β) : (Finset.sum Finset.univ fun (i : Fin 0) => f i) = 0

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

theorem Fin.prod_univ_zero {β : Type u_2} [CommMonoid β] (f : Fin 0 → β) : (Finset.prod Finset.univ fun (i : Fin 0) => f i) = 1

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

theorem Fin.sum_univ_succAbove {β : Type u_2} [AddCommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) (x : Fin (n + 1)) : (Finset.sum Finset.univ fun (i : Fin (n + 1)) => f i) = f x + Finset.sum Finset.univ fun (i : Fin n) => f (Fin.succAbove x 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

theorem Fin.prod_univ_succAbove {β : Type u_2} [CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) (x : Fin (n + 1)) : (Finset.prod Finset.univ fun (i : Fin (n + 1)) => f i) = f x * Finset.prod Finset.univ fun (i : Fin n) => f (Fin.succAbove x 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

theorem Fin.sum_univ_succ {β : Type u_2} [AddCommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) : (Finset.sum Finset.univ fun (i : Fin (n + 1)) => f i) = f 0 + Finset.sum Finset.univ fun (i : Fin n) => f (Fin.succ i)

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

theorem Fin.prod_univ_succ {β : Type u_2} [CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) : (Finset.prod Finset.univ fun (i : Fin (n + 1)) => f i) = f 0 * Finset.prod Finset.univ fun (i : Fin n) => f (Fin.succ i)

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

theorem Fin.sum_univ_castSucc {β : Type u_2} [AddCommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) : (Finset.sum Finset.univ fun (i : Fin (n + 1)) => f i) = (Finset.sum Finset.univ fun (i : Fin n) => f (Fin.castSucc 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

theorem Fin.prod_univ_castSucc {β : Type u_2} [CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) : (Finset.prod Finset.univ fun (i : Fin (n + 1)) => f i) = (Finset.prod Finset.univ fun (i : Fin n) => f (Fin.castSucc 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

theorem Fin.sum_cons {β : Type u_2} [AddCommMonoid β] {n : ℕ} (x : β) (f : Fin n → β) : (Finset.sum Finset.univ fun (i : Fin (Nat.succ n)) => Fin.cons x f i) = x + Finset.sum Finset.univ fun (i : Fin n) => f i

theorem Fin.prod_cons {β : Type u_2} [CommMonoid β] {n : ℕ} (x : β) (f : Fin n → β) : (Finset.prod Finset.univ fun (i : Fin (Nat.succ n)) => Fin.cons x f i) = x * Finset.prod Finset.univ fun (i : Fin n) => f i

theorem Fin.sum_univ_one {β : Type u_2} [AddCommMonoid β] (f : Fin 1 → β) : (Finset.sum Finset.univ fun (i : Fin 1) => f i) = f 0

theorem Fin.prod_univ_one {β : Type u_2} [CommMonoid β] (f : Fin 1 → β) : (Finset.prod Finset.univ fun (i : Fin 1) => f i) = f 0

@[simp]

theorem Fin.sum_univ_two {β : Type u_2} [AddCommMonoid β] (f : Fin 2 → β) : (Finset.sum Finset.univ fun (i : Fin 2) => f i) = f 0 + f 1

@[simp]

theorem Fin.prod_univ_two {β : Type u_2} [CommMonoid β] (f : Fin 2 → β) : (Finset.prod Finset.univ fun (i : Fin 2) => f i) = f 0 * f 1

theorem Fin.sum_univ_three {β : Type u_2} [AddCommMonoid β] (f : Fin 3 → β) : (Finset.sum Finset.univ fun (i : Fin 3) => f i) = f 0 + f 1 + f 2

theorem Fin.prod_univ_three {β : Type u_2} [CommMonoid β] (f : Fin 3 → β) : (Finset.prod Finset.univ fun (i : Fin 3) => f i) = f 0 * f 1 * f 2

theorem Fin.sum_univ_four {β : Type u_2} [AddCommMonoid β] (f : Fin 4 → β) : (Finset.sum Finset.univ fun (i : Fin 4) => f i) = f 0 + f 1 + f 2 + f 3

theorem Fin.prod_univ_four {β : Type u_2} [CommMonoid β] (f : Fin 4 → β) : (Finset.prod Finset.univ fun (i : Fin 4) => f i) = f 0 * f 1 * f 2 * f 3

theorem Fin.sum_univ_five {β : Type u_2} [AddCommMonoid β] (f : Fin 5 → β) : (Finset.sum Finset.univ fun (i : Fin 5) => f i) = f 0 + f 1 + f 2 + f 3 + f 4

theorem Fin.prod_univ_five {β : Type u_2} [CommMonoid β] (f : Fin 5 → β) : (Finset.prod Finset.univ fun (i : Fin 5) => f i) = f 0 * f 1 * f 2 * f 3 * f 4

theorem Fin.sum_univ_six {β : Type u_2} [AddCommMonoid β] (f : Fin 6 → β) : (Finset.sum Finset.univ fun (i : Fin 6) => f i) = f 0 + f 1 + f 2 + f 3 + f 4 + f 5

theorem Fin.prod_univ_six {β : Type u_2} [CommMonoid β] (f : Fin 6 → β) : (Finset.prod Finset.univ fun (i : Fin 6) => f i) = f 0 * f 1 * f 2 * f 3 * f 4 * f 5

theorem Fin.sum_univ_seven {β : Type u_2} [AddCommMonoid β] (f : Fin 7 → β) : (Finset.sum Finset.univ fun (i : Fin 7) => f i) = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6

theorem Fin.prod_univ_seven {β : Type u_2} [CommMonoid β] (f : Fin 7 → β) : (Finset.prod Finset.univ fun (i : Fin 7) => f i) = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6

theorem Fin.sum_univ_eight {β : Type u_2} [AddCommMonoid β] (f : Fin 8 → β) : (Finset.sum Finset.univ fun (i : Fin 8) => f i) = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6 + f 7

theorem Fin.prod_univ_eight {β : Type u_2} [CommMonoid β] (f : Fin 8 → β) : (Finset.prod Finset.univ fun (i : Fin 8) => f i) = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7

theorem Fin.sum_pow_mul_eq_add_pow {n : ℕ} {R : Type u_3} [CommSemiring R] (a : R) (b : R) : (Finset.sum Finset.univ fun (s : Finset (Fin n)) => a ^ s.card * b ^ (n - s.card)) = (a + b) ^ n

theorem Fin.prod_const {α : Type u_1} [CommMonoid α] (n : ℕ) (x : α) : (Finset.prod Finset.univ fun (_i : Fin n) => x) = x ^ n

theorem Fin.sum_const {α : Type u_1} [AddCommMonoid α] (n : ℕ) (x : α) : (Finset.sum Finset.univ fun (_i : Fin n) => x) = n • x

theorem Fin.sum_Ioi_zero {M : Type u_3} [AddCommMonoid M] {n : ℕ} {v : Fin (Nat.succ n) → M} : (Finset.sum (Finset.Ioi 0) fun (i : Fin (Nat.succ n)) => v i) = Finset.sum Finset.univ fun (j : Fin n) => v (Fin.succ j)

theorem Fin.prod_Ioi_zero {M : Type u_3} [CommMonoid M] {n : ℕ} {v : Fin (Nat.succ n) → M} : (Finset.prod (Finset.Ioi 0) fun (i : Fin (Nat.succ n)) => v i) = Finset.prod Finset.univ fun (j : Fin n) => v (Fin.succ j)

theorem Fin.sum_Ioi_succ {M : Type u_3} [AddCommMonoid M] {n : ℕ} (i : Fin n) (v : Fin (Nat.succ n) → M) : (Finset.sum (Finset.Ioi (Fin.succ i)) fun (j : Fin (Nat.succ n)) => v j) = Finset.sum (Finset.Ioi i) fun (j : Fin n) => v (Fin.succ j)

theorem Fin.prod_Ioi_succ {M : Type u_3} [CommMonoid M] {n : ℕ} (i : Fin n) (v : Fin (Nat.succ n) → M) : (Finset.prod (Finset.Ioi (Fin.succ i)) fun (j : Fin (Nat.succ n)) => v j) = Finset.prod (Finset.Ioi i) fun (j : Fin n) => v (Fin.succ j)

theorem Fin.sum_congr' {M : Type u_3} [AddCommMonoid M] {a : ℕ} {b : ℕ} (f : Fin b → M) (h : a = b) : (Finset.sum Finset.univ fun (i : Fin a) => f (Fin.cast h i)) = Finset.sum Finset.univ fun (i : Fin b) => f i

theorem Fin.prod_congr' {M : Type u_3} [CommMonoid M] {a : ℕ} {b : ℕ} (f : Fin b → M) (h : a = b) : (Finset.prod Finset.univ fun (i : Fin a) => f (Fin.cast h i)) = Finset.prod Finset.univ fun (i : Fin b) => f i

theorem Fin.sum_univ_add {M : Type u_3} [AddCommMonoid M] {a : ℕ} {b : ℕ} (f : Fin (a + b) → M) : (Finset.sum Finset.univ fun (i : Fin (a + b)) => f i) = (Finset.sum Finset.univ fun (i : Fin a) => f (Fin.castAdd b i)) + Finset.sum Finset.univ fun (i : Fin b) => f (Fin.natAdd a i)

theorem Fin.prod_univ_add {M : Type u_3} [CommMonoid M] {a : ℕ} {b : ℕ} (f : Fin (a + b) → M) : (Finset.prod Finset.univ fun (i : Fin (a + b)) => f i) = (Finset.prod Finset.univ fun (i : Fin a) => f (Fin.castAdd b i)) * Finset.prod Finset.univ fun (i : Fin b) => f (Fin.natAdd a i)

theorem Fin.sum_trunc {M : Type u_3} [AddCommMonoid M] {a : ℕ} {b : ℕ} (f : Fin (a + b) → M) (hf : ∀ (j : Fin b), f (Fin.natAdd a j) = 0) : (Finset.sum Finset.univ fun (i : Fin (a + b)) => f i) = Finset.sum Finset.univ fun (i : Fin a) => f (Fin.castLE (_ : a ≤ a + b) i)

theorem Fin.prod_trunc {M : Type u_3} [CommMonoid M] {a : ℕ} {b : ℕ} (f : Fin (a + b) → M) (hf : ∀ (j : Fin b), f (Fin.natAdd a j) = 1) : (Finset.prod Finset.univ fun (i : Fin (a + b)) => f i) = Finset.prod Finset.univ fun (i : Fin a) => f (Fin.castLE (_ : a ≤ a + b) i)

def Fin.partialSum {α : Type u_1} [AddMonoid α] {n : ℕ} (f : Fin n → α) (i : Fin (n + 1)) : α

For f = (a₁, ..., aₙ) in αⁿ, partialSum f is

(0, a₁, a₁ + a₂, ..., a₁ + ... + aₙ) in αⁿ⁺¹.

Equations

• Fin.partialSum f i = List.sum (List.take (↑i) (List.ofFn f))

def Fin.partialProd {α : Type u_1} [Monoid α] {n : ℕ} (f : Fin n → α) (i : Fin (n + 1)) : α

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

Equations

• Fin.partialProd f i = List.prod (List.take (↑i) (List.ofFn f))

@[simp]

theorem Fin.partialSum_zero {α : Type u_1} [AddMonoid α] {n : ℕ} (f : Fin n → α) : Fin.partialSum f 0 = 0

@[simp]

theorem Fin.partialProd_zero {α : Type u_1} [Monoid α] {n : ℕ} (f : Fin n → α) : Fin.partialProd f 0 = 1

theorem Fin.partialSum_succ {α : Type u_1} [AddMonoid α] {n : ℕ} (f : Fin n → α) (j : Fin n) : Fin.partialSum f (Fin.succ j) = Fin.partialSum f (Fin.castSucc j) + f j

theorem Fin.partialProd_succ {α : Type u_1} [Monoid α] {n : ℕ} (f : Fin n → α) (j : Fin n) : Fin.partialProd f (Fin.succ j) = Fin.partialProd f (Fin.castSucc j) * f j

theorem Fin.partialSum_succ' {α : Type u_1} [AddMonoid α] {n : ℕ} (f : Fin (n + 1) → α) (j : Fin (n + 1)) : Fin.partialSum f (Fin.succ j) = f 0 + Fin.partialSum (Fin.tail f) j

theorem Fin.partialProd_succ' {α : Type u_1} [Monoid α] {n : ℕ} (f : Fin (n + 1) → α) (j : Fin (n + 1)) : Fin.partialProd f (Fin.succ j) = f 0 * Fin.partialProd (Fin.tail f) j

theorem Fin.partialSum_left_neg {n : ℕ} {G : Type u_3} [AddGroup G] (f : Fin (n + 1) → G) : (f 0 +ᵥ Fin.partialSum fun (i : Fin n) => -f ↑↑i + f (Fin.succ i)) = f

theorem Fin.partialProd_left_inv {n : ℕ} {G : Type u_3} [Group G] (f : Fin (n + 1) → G) : (f 0 • Fin.partialProd fun (i : Fin n) => (f ↑↑i)⁻¹ * f (Fin.succ i)) = f

theorem Fin.partialSum_right_neg {n : ℕ} {G : Type u_3} [AddGroup G] (f : Fin n → G) (i : Fin n) : -Fin.partialSum f (Fin.castSucc i) + Fin.partialSum f (Fin.succ i) = f i

theorem Fin.partialProd_right_inv {n : ℕ} {G : Type u_3} [Group G] (f : Fin n → G) (i : Fin n) : (Fin.partialProd f (Fin.castSucc i))⁻¹ * Fin.partialProd f (Fin.succ i) = f i

theorem Fin.neg_partialSum_add_eq_contractNth {n : ℕ} {G : Type u_3} [AddGroup G] (g : Fin (n + 1) → G) (j : Fin (n + 1)) (k : Fin n) : -Fin.partialSum g (Fin.succAbove (Fin.succ j) (Fin.castSucc k)) + Fin.partialSum g (Fin.succ (Fin.succAbove j k)) = Fin.contractNth j (fun (x x_1 : G) => x + x_1) 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.

theorem Fin.inv_partialProd_mul_eq_contractNth {n : ℕ} {G : Type u_3} [Group G] (g : Fin (n + 1) → G) (j : Fin (n + 1)) (k : Fin n) : (Fin.partialProd g (Fin.succAbove (Fin.succ j) (Fin.castSucc k)))⁻¹ * Fin.partialProd g (Fin.succ (Fin.succAbove j k)) = Fin.contractNth j (fun (x x_1 : G) => x * x_1) 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.

@[simp]

theorem finFunctionFinEquiv_apply_val {m : ℕ} {n : ℕ} (f : Fin n → Fin m) : ↑(finFunctionFinEquiv f) = Finset.sum Finset.univ fun (i : Fin n) => ↑(f i) * m ^ ↑i

@[simp]

theorem finFunctionFinEquiv_symm_apply_val {m : ℕ} {n : ℕ} (a : Fin (m ^ n)) (b : Fin n) : ↑(finFunctionFinEquiv.symm a b) = ↑a / m ^ ↑b % m

def finFunctionFinEquiv {m : ℕ} {n : ℕ} : (Fin n → Fin m) ≃ Fin (m ^ n)

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

Equations

• One or more equations did not get rendered due to their size.

theorem finFunctionFinEquiv_apply {m : ℕ} {n : ℕ} (f : Fin n → Fin m) : ↑(finFunctionFinEquiv f) = Finset.sum Finset.univ fun (i : Fin n) => ↑(f i) * m ^ ↑i

theorem finFunctionFinEquiv_single {m : ℕ} {n : ℕ} [NeZero m] (i : Fin n) (j : Fin m) : ↑(finFunctionFinEquiv (Pi.single i j)) = ↑j * m ^ ↑i

def finPiFinEquiv {m : ℕ} {n : Fin m → ℕ} : ((i : Fin m) → Fin (n i)) ≃ Fin (Finset.prod Finset.univ fun (i : Fin m) => n i)

Equivalence between ∀ i : Fin m, Fin (n i) and Fin (∏ i : Fin m, n i).

Equations

• One or more equations did not get rendered due to their size.

theorem finPiFinEquiv_apply {m : ℕ} {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)) : ↑(finPiFinEquiv f) = Finset.sum Finset.univ fun (i : Fin m) => ↑(f i) * Finset.prod Finset.univ fun (j : Fin ↑i) => n (Fin.castLE (_ : ↑i ≤ m) j)

theorem finPiFinEquiv_single {m : ℕ} {n : Fin m → ℕ} [∀ (i : Fin m), NeZero (n i)] (i : Fin m) (j : Fin (n i)) : ↑(finPiFinEquiv (Pi.single i j)) = ↑j * Finset.prod Finset.univ fun (j : Fin ↑i) => n (Fin.castLE (_ : ↑i ≤ m) j)

theorem List.sum_take_ofFn {α : Type u_1} [AddCommMonoid α] {n : ℕ} (f : Fin n → α) (i : ℕ) : List.sum (List.take i (List.ofFn f)) = Finset.sum (Finset.filter (fun (j : Fin n) => ↑j < i) Finset.univ) fun (j : Fin n) => f j

theorem List.prod_take_ofFn {α : Type u_1} [CommMonoid α] {n : ℕ} (f : Fin n → α) (i : ℕ) : List.prod (List.take i (List.ofFn f)) = Finset.prod (Finset.filter (fun (j : Fin n) => ↑j < i) Finset.univ) fun (j : Fin n) => f j

theorem List.sum_ofFn {α : Type u_1} [AddCommMonoid α] {n : ℕ} {f : Fin n → α} : List.sum (List.ofFn f) = Finset.sum Finset.univ fun (i : Fin n) => f i

theorem List.prod_ofFn {α : Type u_1} [CommMonoid α] {n : ℕ} {f : Fin n → α} : List.prod (List.ofFn f) = Finset.prod Finset.univ fun (i : Fin n) => f i

abbrev List.alternatingSum_eq_finset_sum.match_1 {G : Type u_1} (motive : List G → Prop) : ∀ (x : List G), (Unit → motive []) → (∀ (g : G), motive [g]) → (∀ (g h : G) (L : List G), motive (g :: h :: L)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

theorem List.alternatingSum_eq_finset_sum {G : Type u_3} [AddCommGroup G] (L : List G) : List.alternatingSum L = Finset.sum Finset.univ fun (i : Fin (List.length L)) => (-1) ^ ↑i • List.get L i

theorem List.alternatingProd_eq_finset_prod {G : Type u_3} [CommGroup G] (L : List G) : List.alternatingProd L = Finset.prod Finset.univ fun (i : Fin (List.length L)) => List.get L i ^ (-1) ^ ↑i