Subsum conditions

def SSC {n : ℕ} (a : Fin n → ℤ) : Prop

The subsum condition: any subset of the tuple summing to 0 is either empty or the whole tuple.

Equations

• SSC a = ∀ (b : Finset (Fin n)), b.Nonempty → bᶜ.Nonempty → ∑ i ∈ b, a i ≠ 0

def IsSubsumBlock {n : ℕ} (a : Fin n → ℤ) (s : Finset (Fin n)) : Prop

A subsum block for a is an index set that must be constant in any sign weighting of the tuple's elements that leads to a zero sum.

Equations

• IsSubsumBlock a s = ∀ (b : Fin n → SignType), ∑ i : Fin n, ↑(b i) * a i = 0 → ∃ (c : SignType), ∀ i ∈ s, b i = c

def StrongSSC {n : ℕ} (a : Fin n → ℤ) : Prop

The strong subsum condition, defined as all Fin n being a subsum block.

Equations

• StrongSSC a = IsSubsumBlock a Finset.univ

theorem StrongSSC.SSC {n : ℕ} {a : Fin n → ℤ} (h : StrongSSC a) : _root_.SSC a

theorem SSC.ne_zero {n : ℕ} {a : Fin n → ℤ} (ha : SSC a) (hn : 2 ≤ n) {i : Fin n} : a i ≠ 0

theorem StrongSSC.ne_zero {n : ℕ} {a : Fin n → ℤ} (ha : StrongSSC a) (hn : 2 ≤ n) {i : Fin n} : a i ≠ 0

theorem StrongSSC.perm {n : ℕ} {a : Fin n → ℤ} (h : StrongSSC a) (e : Equiv.Perm (Fin n)) : StrongSSC (a ∘ ⇑e)

theorem strongSSC_perm_iff {n : ℕ} {a : Fin n → ℤ} (e : Equiv.Perm (Fin n)) : StrongSSC a ↔ StrongSSC (a ∘ ⇑e)

theorem StrongSSC.injective {n : ℕ} {a : Fin n → ℤ} (h : StrongSSC a) : Function.Injective a

theorem Finset.natAbs_prod {ι : Type u_1} {s : Finset ι} {f : ι → ℤ} : (∏ i ∈ s, f i).natAbs = ∏ i ∈ s, (f i).natAbs

Upstreamable to mathlib! [Mathlib.Algebra.BigOperators.Group.Finset.Basic]

theorem StrongSSC.one_lt_natAbs_prod {n : ℕ} {a : Fin n → ℤ} (ha : StrongSSC a) (hn : 3 ≤ n) : 1 < (∏ i : Fin n, a i).natAbs

def complRank {n k : ℕ} (s : Finset (Fin n)) (hk : k = n - s.card) (i : Fin k) : Fin n

The order-preserving bijection from Fin k to sᶜ, where k = n - #s.

Equations

• complRank s hk i = (sᶜ.orderEmbOfFin ⋯) (Fin.cast hk i)

theorem complRank_01 {n : ℕ} : complRank {0, 1} ⋯ = fun (x : Fin n) => x.addNat 2

def tupReduce {n k : ℕ} (a : Fin n → ℤ) (s : Finset (Fin n)) (hk : k = n - s.card) : Fin (k + 1) → ℤ

tupReduce a s hk is the tuple with ∑ i ∈ s, a i at the last index and the remaining elements of a appended in order. hk : k = n - #s mitigates definitional equality problems.

Equations

• tupReduce a s hk i = Fin.lastCases (∑ i ∈ s, a i) (fun (i : Fin k) => a (complRank s hk i)) i

theorem injective_complRank {n k : ℕ} {s : Finset (Fin n)} {hk : k = n - s.card} : Function.Injective (complRank s hk)

theorem image_complRank_univ {n k : ℕ} {s : Finset (Fin n)} {hk : k = n - s.card} : Finset.image (complRank s hk) Finset.univ = sᶜ

theorem IsSubsumBlock.empty {n : ℕ} {a : Fin n → ℤ} : IsSubsumBlock a ∅

theorem IsSubsumBlock.singleton {n : ℕ} {a : Fin n → ℤ} {i : Fin n} : IsSubsumBlock a {i}

theorem IsSubsumBlock.subset {n : ℕ} {a : Fin n → ℤ} {s t : Finset (Fin n)} (hs : IsSubsumBlock a s) (ht : t ⊆ s) : IsSubsumBlock a t

theorem IsSubsumBlock.union {n : ℕ} {a : Fin n → ℤ} {s t : Finset (Fin n)} (hs : IsSubsumBlock a s) (ht : IsSubsumBlock a t) (hd : ¬Disjoint s t) : IsSubsumBlock a (s ∪ t)

theorem IsSubsumBlock.of_sum_natAbs_lt {n k : ℕ} {a : Fin n → ℤ} (f : Fin k ↪ Fin n) (hf : ∀ (b : Fin k → SignType), (¬∃ (c : SignType), ∀ (i : Fin k), b i = c) → ∑ i ∈ (Finset.map f Finset.univ)ᶜ, (a i).natAbs < (∑ i : Fin k, ↑(b i) * a (f i)).natAbs) : IsSubsumBlock a (Finset.map f Finset.univ)

theorem IsSubsumBlock.pair_of_sum_natAbs_lt {n : ℕ} {a : Fin n → ℤ} {i j : Fin n} (hi : ∑ k ∈ {i, j}ᶜ, (a k).natAbs < (a i).natAbs) (hj : ∑ k ∈ {i, j}ᶜ, (a k).natAbs < (a j).natAbs) (hprod : a i * a j ≤ 0) : IsSubsumBlock a {i, j}

If there are two elements of opposite signs, each dominating the remaining n - 2 elements (in the sense of violating the triangle inequality), the two elements form a subsum block.

theorem IsSubsumBlock.strongSSC_tupReduce {n k : ℕ} {a : Fin n → ℤ} {s : Finset (Fin n)} (p : IsSubsumBlock a s) (hk : k = n - s.card) (h : StrongSSC (tupReduce a s hk)) : StrongSSC a

Reduce a subsum block to a single element when proving the strong subsum condition.