Completing a family of disjoint exchanges to a zero sum

A family of exchanges which covers a quotient fibre can be combined with prescribed filler counts. Disjointness of multiset positions is expressed by a pointwise capacity bound on all reserved multiplicities.

noncomputable def EGZ.Expansion.vectorSum {G : Type u_1} [AddCommMonoid G] [Fintype G] (u : G → ℕ) : G

The sum of the group elements counted with their natural-number multiplicities.

Equations

• EGZ.Expansion.vectorSum u = ∑ v : G, u v • v

theorem EGZ.Expansion.vectorSum_add {G : Type u_1} [AddCommMonoid G] [Fintype G] (u w : G → ℕ) : vectorSum (u + w) = vectorSum u + vectorSum w

theorem EGZ.Expansion.vectorSum_sum {I : Type u_1} {G : Type u_2} [Fintype I] [Fintype G] [AddCommMonoid G] (u : I → G → ℕ) : vectorSum (∑ i : I, u i) = ∑ i : I, vectorSum (u i)

theorem EGZ.Expansion.map_vectorSum {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [AddCommMonoid H] [Fintype G] [Fintype H] (π : G →+ H) (u : G → ℕ) : π (vectorSum u) = vectorSum (pushWeight (⇑π) u)

noncomputable def EGZ.Expansion.choiceWeight {I : Type u_1} {G : Type u_2} [Fintype I] (left right : I → G → ℕ) (choice : I → Bool) : G → ℕ

The total weight obtained by choosing the left or right weight at each index.

Equations

• EGZ.Expansion.choiceWeight left right choice = ∑ i : I, if choice i = true then left i else right i

theorem EGZ.Expansion.choiceWeight_le {I : Type u_1} {G : Type u_2} [Fintype I] (left right : I → G → ℕ) (choice : I → Bool) : choiceWeight left right choice ≤ ∑ i : I, left i + ∑ i : I, right i

theorem EGZ.Expansion.natMass_choiceWeight {I : Type u_1} {G : Type u_2} [Fintype I] [Fintype G] (left right : I → G → ℕ) (choice : I → Bool) (h : ∀ (i : I), natMass (left i) = natMass (right i)) : natMass (choiceWeight left right choice) = natMass (∑ i : I, left i)

theorem EGZ.Expansion.vectorSum_choiceWeight {I : Type u_1} {G : Type u_2} [Fintype I] [Fintype G] [AddCommGroup G] (left right : I → G → ℕ) (choice : I → Bool) : vectorSum (choiceWeight left right choice) = vectorSum (∑ i : I, right i) + ∑ i : I, if choice i = true then vectorSum (left i) - vectorSum (right i) else 0

theorem EGZ.Expansion.complete_exchange_family {G : Type u_1} {H : Type u_2} {I : Type u_3} [AddCommGroup G] [AddCommGroup H] [Fintype G] [Fintype H] [Fintype I] (π : G →+ H) (w : G → ℕ) (a : H → ℕ) (left right : I → G → ℕ) (hcapacity : ∑ i : I, left i + ∑ i : I, right i ≤ w) (hmass : ∀ (i : I), natMass (left i) = natMass (right i)) (hlo : pushWeight (⇑π) (∑ i : I, left i) ≤ a) (hhi : a + pushWeight (⇑π) (∑ i : I, right i) ≤ pushWeight (⇑π) w) (hzero : vectorSum a = 0) (hcover : ∀ (v : G), π v = π (vectorSum (∑ i : I, left i)) → ∃ (c : I → Bool), vectorSum (choiceWeight left right c) = v) : ∃ u ≤ w, natMass u = natMass a ∧ vectorSum u = 0

A full quotient fibre of possible exchange sums gives a zero sum once the remaining prescribed counts fit outside all reserved positions.

theorem EGZ.Expansion.complete_exchange_family_of_differences {G : Type u_1} {H : Type u_2} {I : Type u_3} [AddCommGroup G] [AddCommGroup H] [Fintype G] [Fintype H] [Fintype I] (π : G →+ H) (w : G → ℕ) (a : H → ℕ) (left right : I → G → ℕ) (hcapacity : ∑ i : I, left i + ∑ i : I, right i ≤ w) (hmass : ∀ (i : I), natMass (left i) = natMass (right i)) (hquotient : ∀ (i : I), π (vectorSum (left i)) = π (vectorSum (right i))) (hlo : pushWeight (⇑π) (∑ i : I, left i) ≤ a) (hhi : a + pushWeight (⇑π) (∑ i : I, right i) ≤ pushWeight (⇑π) w) (hzero : vectorSum a = 0) (hcover : ∀ (v : G), π v = 0 → ∃ (c : I → Bool), (∑ i : I, if c i = true then vectorSum (left i) - vectorSum (right i) else 0) = v) : ∃ u ≤ w, natMass u = natMass a ∧ vectorSum u = 0

The equivalent form used by translation growth: binary sums of the exchange differences cover the quotient kernel.