Sums and products over pairs

A sum of F : l × l → M over all ordered pairs, for l a finite linear order, can be folded onto the increasing pairs by adding each term to its transpose. When F vanishes on the diagonal the diagonal contributes nothing and the fold is exact, which is TauCeti.sum_univ_prod_eq_sum_lt_add_swap.

This is the shape a sum indexed by unordered pairs takes once the linear order is used to name each pair by its increasing representative. It is what lets an antisymmetric summand, for which the two terms of a transposed pair combine, be summed over pairs rather than over ordered pairs.

For a symmetric summand the increasing representative carries no information beyond the unordered pair, so a product ∏_{i<j} f i j over the increasing pairs is unchanged when the indices are permuted, which is TauCeti.prod_prod_Ioi_comp_perm. This is the symmetric counterpart of Mathlib's Equiv.Perm.prod_Ioi_comp_eq_sign_mul_prod, where an antisymmetric summand picks up the sign of the permutation.

Main results

• TauCeti.sum_univ_prod_eq_sum_lt_add_swap: a sum over all ordered pairs of a function vanishing on the diagonal, as a sum over the increasing pairs of the term plus its transpose.
• TauCeti.prod_prod_Ioi_comp_perm: a product of a symmetric function over the increasing pairs is invariant under permuting the indices.
• TauCeti.prod_prod_Ici_eq_prod_prod_Ioi_mul_prod_diag: a product over weakly increasing pairs separates into the strictly increasing pairs and the diagonal.
• TauCeti.prod_prod_Ioi_eq_of_two: separates the first pair and its cross terms from a product over the increasing pairs of a finite ordinal.
• TauCeti.prod_prod_Ioi_three and TauCeti.prod_prod_Ioi_four: the products over the increasing pairs of Fin 3 and of Fin 4, written out.
• TauCeti.prod_prod_Ioi_snoc: splits the pair product of a tuple with a final entry.
• TauCeti.prod_prod_Ioi_append: the pair product of appended tuples splits into the pair products of each tuple and their cross terms.
• TauCeti.prod_prod_Ioi_append_of_mul: the cross term for a bimultiplicative pairing is the pairing of the products.
• TauCeti.sum_sum_Ioi_append_of_mul: the same for a pairing turning products into sums.
• TauCeti.prod_prod_Ioi_scale: scaling all entries of a pair product for a symmetric bimultiplicative pairing.

theorem TauCeti.sum_fin_product_eq_sum_antidiagonal {M : Type u_1} [AddCommMonoid M] {n d : ℕ} (hd : d < n) (f : Fin n × Fin n → M) (g : ℕ × ℕ → M) (hfg : ∀ (l : Fin n × Fin n), ↑l.1 + ↑l.2 = d → f l = g (↑l.1, ↑l.2)) : ∑ l : Fin n × Fin n with ↑l.1 + ↑l.2 = d, f l = ∑ l ∈ Finset.antidiagonal d, g l

A sum over bounded pairs of indices of total degree less than the bound equals the antidiagonal sum, provided the summands agree under the natural-index coercions.

theorem TauCeti.prod_prod_Ici_eq_prod_prod_Ioi_mul_prod_diag {ι : Type u_1} {M : Type u_2} [PartialOrder ι] [Fintype ι] [LocallyFiniteOrderTop ι] [CommMonoid M] (f : ι → ι → M) : ∏ i : ι, ∏ j ≥ i, f i j = (∏ i : ι, ∏ j > i, f i j) * ∏ i : ι, f i i

A product over weakly increasing pairs splits into the strictly increasing pairs and the diagonal.

theorem TauCeti.prod_prod_Ioi_eq_of_two {M : Type u_1} [CommMonoid M] {m : ℕ} (f : Fin (m + 2) → Fin (m + 2) → M) : ∏ i : Fin (m + 2), ∏ j > i, f i j = f 0 1 * ((∏ k : Fin m, f 0 k.succ.succ) * ∏ k : Fin m, f 1 k.succ.succ) * ∏ i : Fin m, ∏ j > i, f i.succ.succ j.succ.succ

Peel the first two indices off a product over the increasing pairs of Fin (m + 2).

theorem TauCeti.prod_prod_Ioi_three {M : Type u_1} [CommMonoid M] (f : Fin 3 → Fin 3 → M) : ∏ i : Fin 3, ∏ j > i, f i j = f 0 1 * f 0 2 * f 1 2

The product over the three increasing pairs of Fin 3.

theorem TauCeti.prod_prod_Ioi_four {M : Type u_1} [CommMonoid M] (f : Fin 4 → Fin 4 → M) : ∏ i : Fin 4, ∏ j > i, f i j = f 0 1 * f 0 2 * f 0 3 * f 1 2 * f 1 3 * f 2 3

The product over the six increasing pairs of Fin 4.

theorem TauCeti.prod_prod_Ioi_snoc {A : Type u_1} {M : Type u_2} [CommMonoid M] {n : ℕ} (f : A → A → M) (w : Fin n → A) (a : A) : ∏ i : Fin (n + 1), ∏ j > i, f (Fin.snoc w a i) (Fin.snoc w a j) = (∏ i : Fin n, ∏ j > i, f (w i) (w j)) * ∏ i : Fin n, f (w i) a

A pair product on a tuple extended by a final entry splits into the old pairs and the pairings with that entry.

theorem TauCeti.prod_prod_Ioi_append {A : Type u_1} {M : Type u_2} [CommMonoid M] {n m : ℕ} (f : A → A → M) (w : Fin n → A) (v : Fin m → A) : ∏ i : Fin (n + m), ∏ j > i, f (Fin.append w v i) (Fin.append w v j) = ((∏ i : Fin n, ∏ j > i, f (w i) (w j)) * ∏ i : Fin m, ∏ j > i, f (v i) (v j)) * ∏ i : Fin n, ∏ j : Fin m, f (w i) (v j)

The pair product of concatenated tuples is the product over pairs in each tuple and over all pairs with one entry in each tuple.

theorem TauCeti.prod_prod_Ioi_append_of_mul {A : Type u_1} {M : Type u_2} [CommMonoid A] [CommMonoid M] (F : A → A → M) (hone_left : ∀ (b : A), F 1 b = 1) (hone_right : ∀ (a : A), F a 1 = 1) (hmul_left : ∀ (a b c : A), F (a * b) c = F a c * F b c) (hmul_right : ∀ (a b c : A), F a (b * c) = F a b * F a c) {m n : ℕ} (p : Fin m → A) (q : Fin n → A) : ∏ i : Fin (m + n), ∏ j > i, F (Fin.append p q i) (Fin.append p q j) = ((∏ i : Fin m, ∏ j > i, F (p i) (p j)) * ∏ i : Fin n, ∏ j > i, F (q i) (q j)) * F (∏ i : Fin m, p i) (∏ j : Fin n, q j)

The pairwise product of a concatenation for a bimultiplicative pairing.

theorem TauCeti.sum_sum_Ioi_append_of_mul {A : Type u_1} {M : Type u_2} [CommMonoid A] [AddCommMonoid M] (F : A → A → M) (hone_left : ∀ (b : A), F 1 b = 0) (hone_right : ∀ (a : A), F a 1 = 0) (hmul_left : ∀ (a b c : A), F (a * b) c = F a c + F b c) (hmul_right : ∀ (a b c : A), F a (b * c) = F a b + F a c) {m n : ℕ} (p : Fin m → A) (q : Fin n → A) : ∑ i : Fin (m + n), ∑ j > i, F (Fin.append p q i) (Fin.append p q j) = ∑ i : Fin m, ∑ j > i, F (p i) (p j) + ∑ i : Fin n, ∑ j > i, F (q i) (q j) + F (∏ i : Fin m, p i) (∏ j : Fin n, q j)

The pairwise sum of a concatenation for a pairing that turns products in either argument into sums.

theorem TauCeti.prod_prod_Ioi_scale {A : Type u_1} {M : Type u_2} [CommMonoid A] [CommMonoid M] (F : A → A → M) {s : A} (hmul_right : ∀ (a b c : A), F a (b * c) = F a b * F a c) (hcomm : ∀ (a b : A), F a b = F b a) (a : A) (hself : F a a = F a s) {n : ℕ} (w : Fin n → A) : ∏ i : Fin n, ∏ j > i, F (a * w i) (a * w j) = (∏ i : Fin n, ∏ j > i, F (w i) (w j)) * F a s ^ n.choose 2 * F a (∏ i : Fin n, w i) ^ (n - 1)

Scaling every coefficient in a pairwise product for a symmetric bimultiplicative pairing. The self-pairing law supplies the correction for each coefficient pair.

theorem TauCeti.sum_univ_prod_eq_sum_lt_add_swap {l : Type u_1} [Fintype l] [LinearOrder l] {M : Type u_2} [AddCommMonoid M] (F : l × l → M) (hdiag : ∀ (a : l), F (a, a) = 0) : ∑ ij : l × l, F ij = ∑ ij : l × l with ij.1 < ij.2, (F ij + F ij.swap)

A sum over all ordered pairs, folded onto the increasing ones. A function vanishing on the diagonal sums over l × l to the sum over the increasing pairs of its value together with its value at the transposed pair.

theorem TauCeti.prod_prod_Ioi_comp_perm {ι : Type u_1} {M : Type u_2} [LinearOrder ι] [Fintype ι] [LocallyFiniteOrderTop ι] [CommMonoid M] (f : ι → ι → M) (σ : Equiv.Perm ι) (hf : ∀ (i j : ι), f i j = f j i) : ∏ i : ι, ∏ j > i, f (σ i) (σ j) = ∏ i : ι, ∏ j > i, f i j

A product over the increasing pairs of a symmetric function is permutation invariant: for symmetric f, ∏_{i<j} f (σ i) (σ j) = ∏_{i<j} f i j for every permutation σ.

theorem TauCeti.sum_sum_Ioi_comp_perm {ι : Type u_1} {M : Type u_2} [LinearOrder ι] [Fintype ι] [LocallyFiniteOrderTop ι] [AddCommMonoid M] (f : ι → ι → M) (σ : Equiv.Perm ι) (hf : ∀ (i j : ι), f i j = f j i) : ∑ i : ι, ∑ j > i, f (σ i) (σ j) = ∑ i : ι, ∑ j > i, f i j

A sum over the increasing pairs of a symmetric function is permutation invariant: for symmetric f, ∑_{i<j} f (σ i) (σ j) = ∑_{i<j} f i j for every permutation σ.