Erdős Problem 350

References:

• erdosproblems.com/350
• [BeEr74] Benkoski, S. J. and Erdős, P., On weird and pseudoperfect numbers. Math. Comp. (1974), 617-623.
• [HSS77] Hanson, F. and Steele, J. M. and Stenger, F., Distinct sums over subsets. Proc. Amer. Math. Soc. (1977), 179-180.

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.

This was proved by Ryavec, who did not appear to ever publish the proof. Ryavec's proof is reproduced in [BeEr74]. More generally, Ryavec's proof delivers that $\sum_{n\in A}\frac{1}{n}\leq 2-2^{1-\lvert A\rvert},$ with equality if and only if $A=\{1,2,\ldots,2^k\}$.

This was formalized in Lean by Alexeev using Aristotle.

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 [HSS77].

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.