Zero sums in natural-valued multiplicities

The decomposition and expansion arguments use multiplicity functions. The EGZ constant uses sequences with distinct selected positions. This file supplies the bridge between these two models.

def EGZ.HasZeroSumMultiplicity {p d : ℕ} [NeZero p] (f : FpCoord p d → ℕ) : Prop

A submultiset of exactly p vectors whose sum vanishes.

Equations

• EGZ.HasZeroSumMultiplicity f = ∃ a ≤ f, EGZ.natMass a = p ∧ ∑ v : EGZ.FpCoord p d, a v • v = 0

theorem EGZ.HasZeroSumMultiplicity.mono {p d : ℕ} [NeZero p] {f g : FpCoord p d → ℕ} (h : HasZeroSumMultiplicity f) (hfg : f ≤ g) : HasZeroSumMultiplicity g

noncomputable def EGZ.sequenceMultiplicity {p d : ℕ} {ι : Type u_1} [Fintype ι] (v : ι → FpCoord p d) (q : FpCoord p d) : ℕ

The multiplicity of a vector in a finite indexed sequence.

Equations

• EGZ.sequenceMultiplicity v q = {i : ι | v i = q}.card

theorem EGZ.natMass_sequenceMultiplicity {p d : ℕ} [NeZero p] {ι : Type u_1} [Fintype ι] (v : ι → FpCoord p d) : natMass (sequenceMultiplicity v) = Fintype.card ι

theorem EGZ.hasZeroSumSubsequence_of_multiplicity {p d : ℕ} [NeZero p] {ι : Type u_1} [Fintype ι] (v : ι → FpCoord p d) (h : HasZeroSumMultiplicity (sequenceMultiplicity v)) : HasZeroSumSubsequence p v

Selecting bounded multiplicities selects distinct sequence positions, even when the vectors at those positions coincide.

theorem EGZ.egzProperty_of_multiplicity {p d n : ℕ} [NeZero p] (h : ∀ (f : FpCoord p d → ℕ), natMass f = n → HasZeroSumMultiplicity f) : EGZProperty p d n

A multiplicity-form estimate at an exact length gives the EGZ property at that length.

theorem EGZ.FlagDecomposition.hasZeroSum_of_cumulative {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (h : HasZeroSumMultiplicity (Φ.cumulativeWeight x)) : HasZeroSumMultiplicity f

A zero sum in a cumulative node is a zero sum in the original input.