def DistinctSums.HasDistinctSubsetSums (S : Finset ℕ) : Prop

A set $S \subseteq \mathbb{N}$ has distinct subset sums if any two subsets with equal sums must be equal.

theorem DistinctSums.erdos_conjecture_distinct_subset_sums : ∃ c > 0, ∀ (k n : ℕ) (S : Finset ℕ), S.card = k → (∀ x ∈ S, 1 ≤ x ∧ x ≤ n) → HasDistinctSubsetSums S → c * 2 ^ k ≤ ↑n

Erdős's conjecture on distinct subset sums (Conjecture 4.6.2): there is an absolute constant $c > 0$ such that any $k$-element set of positive integers in $[1, n]$ with distinct subset sums satisfies $c \cdot 2^k \le n$.

@[reducible, inline]

abbrev HarperIsoperimetric.Hypercube (k : ℕ) : Type

The $k$-dimensional Boolean hypercube $\{0,1\}^k$, represented as functions $\mathrm{Fin}\, k \to \mathrm{Bool}$.

def HarperIsoperimetric.Hypercube.Adjacent {k : ℕ} (x y : Hypercube k) : Prop

Two vertices of the hypercube are adjacent if their Hamming distance is $1$, i.e. they differ in exactly one coordinate.

@[implicit_reducible]

instance HarperIsoperimetric.instDecidableAdjacent {k : ℕ} (x y : Hypercube k) : Decidable (x.Adjacent y)

Decidability instance for adjacency in the hypercube.

def HarperIsoperimetric.Hypercube.vertexBoundary {k : ℕ} (A : Finset (Hypercube k)) : Finset (Hypercube k)

The vertex boundary of a set $A$ in the hypercube: vertices outside $A$ adjacent to some vertex in $A$.

theorem HarperIsoperimetric.harper_vertex_isoperimetric (k : ℕ) (A : Finset (Hypercube k)) (hA : A.card = 2 ^ (k - 1)) : (Hypercube.vertexBoundary A).card ≥ k.choose (k / 2)

Harper's vertex-isoperimetric inequality on the hypercube (Theorem 4.6.4): any set $A \subseteq \{0,1\}^k$ of size $2^{k-1}$ has vertex boundary at least $\binom{k}{\lfloor k/2 \rfloor}$.

def DubroffFoxXu.weightedSum {k : ℕ} (x : Fin k → ℕ) (ε : Fin k → Bool) : ℕ

Weighted sum $\sum_{i : \varepsilon_i = \mathtt{true}} x_i$ selecting coordinates of $x$ indicated by the Boolean string $\varepsilon$.

def DubroffFoxXu.boolCompl {k : ℕ} (ε : Fin k → Bool) : Fin k → Bool

Coordinatewise Boolean complement of $\varepsilon \in \{0,1\}^k$.

def DubroffFoxXu.boolToFinset {k : ℕ} (ε : Fin k → Bool) : Finset (Fin k)

The subset of $\mathrm{Fin}\, k$ on which the Boolean function $\varepsilon$ is true.

def DubroffFoxXu.HasDistinctSubsetSumsFin {k : ℕ} (x : Fin k → ℕ) : Prop

Variant of HasDistinctSubsetSums for tuples $x : \mathrm{Fin}\, k \to \mathbb{N}$: the map sending a subset $T$ to $\sum_{i \in T} x_i$ is injective.

def DubroffFoxXu.cubeBoundary {k : ℕ} (A : Finset (Fin k → Bool)) : Finset (Fin k → Bool)

Vertex boundary of $A$ in the hypercube $\{0,1\}^k$, formulated via differing in exactly one coordinate from some vertex in $A$.

theorem DubroffFoxXu.boolToFinset_injective {k : ℕ} : Function.Injective boolToFinset

The map boolToFinset from Boolean strings to subsets of $\mathrm{Fin}\, k$ is injective.

theorem DubroffFoxXu.weightedSum_eq_sum {k : ℕ} (x : Fin k → ℕ) (ε : Fin k → Bool) : weightedSum x ε = ∑ i ∈ boolToFinset ε, x i

Rewrites the weighted sum as a sum over the subset selected by $\varepsilon$.

theorem DubroffFoxXu.weightedSum_injective {k : ℕ} {x : Fin k → ℕ} (hdist : HasDistinctSubsetSumsFin x) : Function.Injective (weightedSum x)

If $x$ has distinct subset sums, then the map $\varepsilon \mapsto \sum \varepsilon_i x_i$ is injective on Boolean strings.

theorem DubroffFoxXu.weightedSum_add_compl {k : ℕ} (x : Fin k → ℕ) (ε : Fin k → Bool) : weightedSum x ε + weightedSum x (boolCompl ε) = ∑ i : Fin k, x i

A Boolean string and its complement select disjoint pieces whose weighted sums add up to the total $\sum_i x_i$.

theorem DubroffFoxXu.weightedSum_neighbor {k : ℕ} (x : Fin k → ℕ) (ε u : Fin k → Bool) (i : Fin k) (hagree : ∀ (j : Fin k), j ≠ i → ε j = u j) (hε_true : ε i = true) (hu_false : u i = false) : weightedSum x ε = weightedSum x u + x i

If two Boolean strings $\varepsilon, u$ agree off coordinate $i$ with $\varepsilon_i = \mathtt{true}$ and $u_i = \mathtt{false}$, then their weighted sums differ by $x_i$.

theorem DubroffFoxXu.harper_vertex_isoperimetric_v2 {k : ℕ} (A : Finset (Fin k → Bool)) (hA : A.card = 2 ^ (k - 1)) : (cubeBoundary A).card ≥ k.choose (k / 2)

Harper's vertex-isoperimetric inequality on the hypercube (Theorem 4.6.4), variant using cubeBoundary: any subset $A$ of half-size in $\{0,1\}^k$ has vertex boundary at least $\binom{k}{\lfloor k/2 \rfloor}$.

theorem DubroffFoxXu.dubroff_fox_xu {k n : ℕ} (hk : 0 < k) (x : Fin k → ℕ) (hx_pos : ∀ (i : Fin k), 0 < x i) (hx_le : ∀ (i : Fin k), x i ≤ n) (hdist : HasDistinctSubsetSumsFin x) : n ≥ k.choose (k / 2)

Dubroff–Fox–Xu (Theorem 4.6.3): for any $k$ positive integers $x_1,\dots,x_k \le n$ with distinct subset sums, $n \ge \binom{k}{\lfloor k/2 \rfloor}$.

def DistinctSumsBound.boolSign (b : Bool) : ℤ

Sign encoding of a Boolean: $\mathtt{true} \mapsto +1$, $\mathtt{false} \mapsto -1$.

theorem DistinctSumsBound.sum_boolSign_prod (k : ℕ) (l m : Fin k) : ∑ ε : Fin k → Bool, boolSign (ε l) * boolSign (ε m) = if l = m then 2 ^ k else 0

Orthogonality of sign characters over $\{0,1\}^k$: the sum of $\mathrm{sgn}(\varepsilon_l)\,\mathrm{sgn}(\varepsilon_m)$ over all $\varepsilon$ equals $2^k$ if $l = m$ and vanishes otherwise.

theorem DistinctSumsBound.variance_identity (k : ℕ) (x : Fin k → ℤ) : ∑ ε : Fin k → Bool, (∑ l : Fin k, boolSign (ε l) * x l) ^ 2 = 2 ^ k * ∑ l : Fin k, x l ^ 2

Variance identity from second-moment method: $\sum_{\varepsilon \in \{\pm 1\}^k} \bigl(\sum_l \varepsilon_l x_l\bigr)^2 = 2^k \sum_l x_l^2$.

theorem DistinctSumsBound.two_ws_minus_S_eq (k : ℕ) (x : Fin k → ℕ) (ε : Fin k → Bool) : 2 * ↑(DubroffFoxXu.weightedSum x ε) - ∑ i : Fin k, ↑(x i) = ∑ i : Fin k, boolSign (ε i) * ↑(x i)

Conversion to signed sums: $2 \sum_{i : \varepsilon_i} x_i - \sum_i x_i = \sum_i \mathrm{sgn}(\varepsilon_i)\,x_i$.

theorem DistinctSumsBound.distinct_sums_bound {k n : ℕ} (hk : 0 < k) (hn : 0 < n) (x : Fin k → ℕ) (hx_pos : ∀ (i : Fin k), 0 < x i) (hx_le : ∀ (i : Fin k), x i ≤ n) (hdist : DubroffFoxXu.HasDistinctSubsetSumsFin x) : 3 * 2 ^ k ≤ 8 * n * (k.sqrt + 1)

Dubroff–Fox–Xu second-moment bound (Theorem 4.6.6): for any $k$ positive integers $x_1,\dots,x_k \le n$ with distinct subset sums, $3 \cdot 2^k \le 8 n (\lfloor \sqrt{k} \rfloor + 1)$, yielding $n = \Omega(2^k / \sqrt{k})$.