Erdős Problem 350

Reference: erdosproblems.com/350

def Erdos350.DistinctSubsetSums {M : Type u_1} [AddCommMonoid M] (A : Set M) : Prop

The predicate that all (finite) subsets of A have distinct sums

Equations

• Erdos350.DistinctSubsetSums A = {X : Finset M | ↑X ⊆ A}.Pairwise fun (X Y : Finset M) => X.sum id ≠ Y.sum id

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

The predicate that all (finite) subsets of A have distinct sums, decidable version

Equations

• Erdos350.DecidableDistinctSubsetSums A = ∀ X ⊆ A, ∀ Y ⊆ A, X ≠ Y → X.sum id ≠ Y.sum id

theorem Erdos350.decidableDistinctSubsetSums_1_2 : DecidableDistinctSubsetSums {1, 2}

theorem Erdos350.distinctSubsetSums_1_2 : DistinctSubsetSums ↑{1, 2}

theorem Erdos350.DistinctSubsetSums_iff_DecidableDistinctSubsetSums {M : Type u_1} [AddCommMonoid M] [DecidableEq M] (A : Finset M) : DistinctSubsetSums ↑A ↔ DecidableDistinctSubsetSums A

Small sanity check: the two predicates are saying the same thing.

theorem Erdos350.erdos_350 (A : Finset ℕ) (hA : DecidableDistinctSubsetSums A) : ∑ n ∈ A, 1 / ↑n < 2

If A ⊂ ℕ is a finite set of integers all of whose subset sums are distinct then ∑ n ∈ A, 1/n < 2. Proved by Ryavec.

theorem Erdos350.erdos_350.variants.strengthening (A : Finset ℕ) (hA : DecidableDistinctSubsetSums A) (s : ℝ) (hs : 0 < s) : ∑ n ∈ A, (1 / ↑n) ^ s < 1 / (1 - 2 ^ (-s))

If A ⊂ ℕ is a finite set of integers all of whose subset sums are distinct then ∑ n ∈ A, 1/n^s < 1/(1 - 2^(-s)), for any s > 0. Proved by Hanson, Steele, and Stenger.

We exlude here the case s = 0, because in the informal formulation then the right hand side is to be interpreted as ∞, while the left hand side counts the elements in A.