Documentation

Mathlib.Combinatorics.Additive.SubsetSum

Subset sums #

This file defines the subset sum of a finite subset of a commutative monoid.

References #

[Melvyn B. Nathanson, Inverse theorems for subset sums][Nathanson1995]

def Finset.subsetSum {M : Type u_1} [DecidableEq M] [AddCommMonoid M] (A : Finset M) :

The subset-sum of a finite set A in a commutative monoid is the set of all sums of subsets of A.

Equations

A.subsetSum = Finset.image (fun (B : Finset M) => B.sum id) A.powerset

Instances For

theorem Finset.mem_subsetSum_iff {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} {a : M} :

a ∈ A.subsetSum ↔ ∃ B ⊆ A, ∑ b ∈ B, b = a

@[simp]

theorem Finset.zero_mem_subsetSum {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} :

0 ∈ A.subsetSum

@[simp]

theorem Finset.subsetSum_nonempty {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} :

A.subsetSum.Nonempty

theorem Finset.subset_subsetSum {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} :

A ⊆ A.subsetSum

theorem Finset.subsetSum_mono {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A B : Finset M} (hAB : A ⊆ B) :

A.subsetSum ⊆ B.subsetSum

@[simp]

theorem Finset.subsetSum_erase_zero {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} :

(A.erase 0).subsetSum = A.subsetSum

theorem Finset.vadd_finset_subsetSum_subset_subsetSum_insert {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} {a : M} (a_notin_A : a ∉ A) :

a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum

theorem Finset.nonneg_of_mem_subsetSum {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} [LinearOrder M] [IsOrderedCancelAddMonoid M] (A_nonneg : ∀ x ∈ A, 0 ≤ x) (x : M) :

x ∈ A.subsetSum → 0 ≤ x

theorem Finset.card_add_card_subsetSum_lt_card_subsetSum_insert_max {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} {a : M} [LinearOrder M] [IsOrderedCancelAddMonoid M] (hA : ∀ x ∈ A, 0 < x) (hAa : ∀ x ∈ A, x < a) (ha : 0 < a) :

A.card + A.subsetSum.card < (insert a A).subsetSum.card

theorem Finset.card_succ_choose_two_lt_card_subsetSum_of_pos {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} [LinearOrder M] [IsOrderedCancelAddMonoid M] (A_pos : ∀ x ∈ A, 0 < x) :

(A.card + 1).choose 2 < A.subsetSum.card

theorem Finset.card_choose_two_lt_card_subsetSum_of_nonneg {M : Type u_1} [DecidableEq M] [AddCommMonoid M] {A : Finset M} [LinearOrder M] [IsOrderedCancelAddMonoid M] (A_pos : ∀ x ∈ A, 0 ≤ x) :

A.card.choose 2 < A.subsetSum.card