Reindexing double sums over multiplication antidiagonals

For partially well-ordered sets s, t, u in an ordered cancellative commutative monoid, a product over the triples (a, b, c) with a * b * c = d can be computed by first splitting d as a * (b * c) or as (a * b) * c, and also by splitting off b first instead of a. A product over the pairs (a, b) with a * b = d can be indexed with the two factors exchanged. These reindexings underlie associativity-type identities for convolution products of Hahn series.

Main results

• Finset.smulAntidiagonal_eq_mulAntidiagonal, Finset.vaddAntidiagonal_eq_antidiagonal: for a monoid acting on itself, the scalar (vector) antidiagonal is the multiplication (addition) antidiagonal.
• Finset.prod_mulAntidiagonal_swap, Finset.sum_antidiagonal_swap: exchanging the two factors of a product (sum) over an antidiagonal.
• Finset.prod_sigma_mulAntidiagonal_assoc, Finset.sum_sigma_antidiagonal_assoc: reassociating a double product (sum) over antidiagonals.
• Finset.prod_sigma_mulAntidiagonal_left_comm, Finset.sum_sigma_antidiagonal_left_comm: exchanging the first two indices of a double product (sum) over antidiagonals.

The bijections follow the proof of HahnSeries.mul_assoc in Mathlib's Mathlib/RingTheory/HahnSeries/Multiplication.lean.

theorem Finset.smulAntidiagonal_eq_mulAntidiagonal {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (a : α) : SMulAntidiagonal a ⋯ = mulAntidiagonal hs ht a

For a monoid acting on itself by multiplication, the scalar antidiagonal of two partially well-ordered sets is their multiplication antidiagonal.

theorem Finset.vaddAntidiagonal_eq_antidiagonal {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (a : α) : VAddAntidiagonal a ⋯ = antidiagonal hs ht a

For an additive monoid acting on itself by addition, the vector antidiagonal of two partially well-ordered sets is their addition antidiagonal.

theorem Finset.prod_mulAntidiagonal_swap {α : Type u_1} {M : Type u_2} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] [CommMonoid M] {s t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (a : α) (f : α → α → M) : ∏ ij ∈ mulAntidiagonal hs ht a, f ij.1 ij.2 = ∏ ij ∈ mulAntidiagonal ht hs a, f ij.2 ij.1

A product over a multiplication antidiagonal may be indexed with the two factors exchanged.

theorem Finset.sum_antidiagonal_swap {α : Type u_1} {M : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [AddCommMonoid M] {s t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (a : α) (f : α → α → M) : ∑ ij ∈ antidiagonal hs ht a, f ij.1 ij.2 = ∑ ij ∈ antidiagonal ht hs a, f ij.2 ij.1

A sum over an addition antidiagonal may be indexed with the two summands exchanged.

theorem Finset.prod_sigma_mulAntidiagonal_assoc {α : Type u_1} {M : Type u_2} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] [CommMonoid M] {s t u : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (hu : u.IsPWO) (d : α) (F : α → α → α → M) : ∏ p ∈ (mulAntidiagonal hs ⋯ d).sigma fun (p : α × α) => mulAntidiagonal ht hu p.2, F p.fst.1 p.snd.1 p.snd.2 = ∏ p ∈ (mulAntidiagonal ⋯ hu d).sigma fun (p : α × α) => mulAntidiagonal hs ht p.1, F p.snd.1 p.snd.2 p.fst.2

Reassociating a double product over antidiagonals: the products indexed by (a, (b, c)) and by ((a, b), c), with a * b * c = d, agree.

theorem Finset.sum_sigma_antidiagonal_assoc {α : Type u_1} {M : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [AddCommMonoid M] {s t u : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (hu : u.IsPWO) (d : α) (F : α → α → α → M) : ∑ p ∈ (antidiagonal hs ⋯ d).sigma fun (p : α × α) => antidiagonal ht hu p.2, F p.fst.1 p.snd.1 p.snd.2 = ∑ p ∈ (antidiagonal ⋯ hu d).sigma fun (p : α × α) => antidiagonal hs ht p.1, F p.snd.1 p.snd.2 p.fst.2

Reassociating a double sum over antidiagonals: the sums indexed by (a, (b, c)) and by ((a, b), c), with a + b + c = d, agree.

theorem Finset.prod_sigma_mulAntidiagonal_left_comm {α : Type u_1} {M : Type u_2} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] [CommMonoid M] {s t u : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (hu : u.IsPWO) (d : α) (F : α → α → α → M) : ∏ p ∈ (mulAntidiagonal hs ⋯ d).sigma fun (p : α × α) => mulAntidiagonal ht hu p.2, F p.fst.1 p.snd.1 p.snd.2 = ∏ p ∈ (mulAntidiagonal ht ⋯ d).sigma fun (p : α × α) => mulAntidiagonal hs hu p.2, F p.snd.1 p.fst.1 p.snd.2

Exchanging the first two indices of a double product over antidiagonals: the products indexed by (a, (b, c)) and by (b, (a, c)), with a * b * c = d, agree.

theorem Finset.sum_sigma_antidiagonal_left_comm {α : Type u_1} {M : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [AddCommMonoid M] {s t u : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (hu : u.IsPWO) (d : α) (F : α → α → α → M) : ∑ p ∈ (antidiagonal hs ⋯ d).sigma fun (p : α × α) => antidiagonal ht hu p.2, F p.fst.1 p.snd.1 p.snd.2 = ∑ p ∈ (antidiagonal ht ⋯ d).sigma fun (p : α × α) => antidiagonal hs hu p.2, F p.snd.1 p.fst.1 p.snd.2

Exchanging the first two indices of a double sum over antidiagonals: the sums indexed by (a, (b, c)) and by (b, (a, c)), with a + b + c = d, agree.