Distinct subset sums

This file defines finite sets of natural numbers with distinct subset sums and establishes the elementary upper bound on their sum of squares in terms of their largest element.

def LeanPool.ErdosMoser.HasDistinctSubsetSums (A : Finset ℕ) : Prop

A finite set has distinct subset sums if the subset-sum map on its powerset is injective.

Equations

• LeanPool.ErdosMoser.HasDistinctSubsetSums A = ∀ S ∈ A.powerset, ∀ T ∈ A.powerset, S.sum id = T.sum id → S = T

theorem LeanPool.ErdosMoser.powersetCardEqTwoPow (A : Finset ℕ) : A.powerset.card = 2 ^ A.card

The powerset of a finite set has cardinality 2 ^ A.card.

theorem LeanPool.ErdosMoser.sumSquaresLeCardMulMaxSquare {A : Finset ℕ} (hA : A.Nonempty) : ∑ a ∈ A, ↑a ^ 2 ≤ ↑A.card * ↑(A.max' hA) ^ 2

The sum of the squared elements of a nonempty finite set is at most its cardinality times the square of its largest element.