Finite sums with injectively indexed partners

A source finset together with an embedding of its elements into the ambient type determines a family of sources and partners. When partners lie outside the source finset, every pair is counted once. A sum over this family vanishes if the two contributions in every pair sum to zero.

Main results

• Finset.withPartners: the union of a source finset and its injectively indexed partners.
• Finset.mem_withPartners: membership as a source or a partner.
• Finset.sum_withPartners_eq_zero: cancellation of pairwise zero contributions.

def Finset.withPartners {α : Type u_1} [DecidableEq α] (s : Finset α) (e : ↥s ↪ α) : Finset α

A source finset together with its injectively indexed partners.

Equations

• s.withPartners e = s ∪ Finset.map e s.attach

@[simp]

theorem Finset.mem_withPartners {α : Type u_1} [DecidableEq α] (s : Finset α) (e : ↥s ↪ α) (a : α) : a ∈ s.withPartners e ↔ a ∈ s ∨ ∃ (b : ↥s), e b = a

Membership in the paired family is membership as a source or as an indexed partner.

theorem Finset.sum_withPartners_eq_zero {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddCommMonoid M] (s : Finset α) (e : ↥s ↪ α) (f : α → M) (hdisjoint : ∀ (a : ↥s), e a ∉ s) (hzero : ∀ (a : ↥s), f ↑a + f (e a) = 0) : ∑ a ∈ s.withPartners e, f a = 0

A sum over sources and their partners vanishes when partners lie outside the sources and each pair contributes zero. Only an additive commutative monoid is required.