Definition of f_k(S, α)

noncomputable def SubsetSum.subsetSumCount (k : ℕ) (S : Finset ℝ) (α : ℝ) : ℕ

subsetSumCount k S α is the number of k-element subsets of S whose elements sum to α. This is f_k(S, α) in the book's notation.

def SubsetSum.iccNat (n : ℕ) : Finset ℕ

The set {1, 2, ..., n} as a Finset ℕ.

def SubsetSum.subsetSumCountNat (k n α : ℕ) : ℕ

subsetSumCountNat k n α counts the number of k-element subsets of {1,...,n} summing to α. This is f_k([n], α) in the book's notation.

Key Lemma (Claim from Theorem 6.11's proof)

The core combinatorial observation: if we have componentwise ≤ sequences with equal sums, the sequences must be equal. This is the heart of the proof.

theorem SubsetSum.eq_of_le_of_sum_eq {k : ℕ} {x y : Fin k → ℝ} (hle : ∀ (i : Fin k), x i ≤ y i) (hsum : ∑ i : Fin k, x i = ∑ i : Fin k, y i) (i : Fin k) : x i = y i

If x i ≤ y i for all i : Fin k and ∑ i, x i = ∑ i, y i, then x i = y i for all i.

Proof: if any x i₀ < y i₀, then ∑ x i < ∑ y i since all terms satisfy x i ≤ y i with at least one strict, contradicting the equal sums assumption.

theorem SubsetSum.claim_indices_eq {n k : ℕ} {a : Fin n → ℝ} (ha : StrictMono a) {is js : Fin k → Fin n} (h_le : ∀ (r : Fin k), is r ≤ js r) (h_sum : ∑ r : Fin k, a (is r) = ∑ r : Fin k, a (js r)) (r : Fin k) : is r = js r

Claim (Theorem 6.11 proof). If a : Fin n → ℝ is strictly increasing and is, js : Fin k → Fin n satisfy is r ≤ js r for all r with equal composition sums ∑ r, a (is r) = ∑ r, a (js r), then is r = js r for all r.

Proof: strict monotonicity of a gives a(is r) ≤ a(js r) from is r ≤ js r. The lemma eq_of_le_of_sum_eq yields a(is r) = a(js r) for all r. By strict monotonicity (hence injectivity), is r = js r.

theorem SubsetSum.claim_incomparable_of_distinct {n k : ℕ} {a : Fin n → ℝ} (ha : StrictMono a) {is js : Fin k → Fin n} (h_ne : is ≠ js) (h_sum : ∑ r : Fin k, a (is r) = ∑ r : Fin k, a (js r)) : ¬∀ (r : Fin k), is r ≤ js r

Corollary of the claim: two distinct k-element subsets of a strictly increasing sequence with the same sum must have incomparable index partitions.

If T ≠ U are k-subsets with equal sums, neither λ(T*) ≤ λ(U*) nor λ(U*) ≤ λ(T*) in L(k, n-k). This is because λ(T*) ≤ λ(U*) would mean the sorted indices of T are componentwise ≤ those of U. By claim_indices_eq, this forces T = U, contradicting T ≠ U.

Connection to L(k, n-k)

The λ-map bijection gives: f_k([n], α) = p_{α - C(k+1,2)}(k, n-k) (eq. 34). Combined with Corollary 6.10 (Sperner, unimodal, symmetric): maxRankCount(L(k, n-k)) = p_{⌊k(n-k)/2⌋}(k, n-k) = f_k([n], ⌊k(n+1)/2⌋).

The λ-map sends {i₁ < ... < i_k} ⊆ [n] to the partition (i_r - r)_{r=1..k} in L(k, n-k). Under this bijection:

• The componentwise ordering on sorted index sets corresponds to ≤ in L(k, n-k).
• Sum of elements = sum of parts + k(k+1)/2.
• The map is a bijection between C([n], k) and L(k, n-k).

The book proves equation (34) by defining the λ-map and observing the sum shift. The maxRankCount identification uses Corollary 6.10 (unimodality + symmetry → max at middle rank) combined with equation (34) and the arithmetic identity ⌊k(n-k)/2⌋ + k(k+1)/2 = ⌊k(n+1)/2⌋. These proofs require constructing the λ-map bijection as a formal Lean equivalence between powersetCard k (iccNat n) and Lmn k (n - k), which depends on infrastructure not currently formalized (ordered embeddings to antitone functions, sum preservation, etc.).

Helper lemmas for the λ-map bijection

noncomputable def SubsetSum.lambdaMapForward (k m : ℕ) (p : YoungLattice.Lmn k m) : Finset ℕ

The forward map: given a partition p ∈ Lmn k m, produce a k-element subset of {1, ..., k+m} by setting the r-th element to p(rev r) + r + 1.

theorem SubsetSum.subsetSumCountNat_eq_rankCount (k n α : ℕ) (hk : k ≤ n) (hα : k * (k + 1) / 2 ≤ α) : subsetSumCountNat k n α = SpernerProperty.rankCount (α - k * (k + 1) / 2)

theorem SubsetSum.maxRankCount_Lmn_eq (k n : ℕ) (hk : k ≤ n) : SpernerProperty.maxRankCount = subsetSumCountNat k n (k * (n + 1) / 2)

The antichain injection

Equal-sum k-subsets of S map injectively to an antichain in L(k, n-k), so their count is bounded by maxRankCount.

The proof: sort S as a₁ < ... < aₙ, map each k-subset T to its index set T* ⊆ [n], then to λ(T*) ∈ L(k, n-k) via the λ-map. By claim_incomparable_of_distinct, distinct equal-sum subsets give incomparable partitions (an antichain). By Lmn_hasSpernerProperty (Corollary 6.10): antichain size ≤ maxRankCount.

theorem SubsetSum.subsetSumCount_le_maxRankCount (n k : ℕ) (hk : 0 < k) (S : Finset ℝ) (hScard : S.card = n) (hSpos : ∀ x ∈ S, 0 < x) (α : ℝ) (hα : 0 < α) : subsetSumCount k S α ≤ SpernerProperty.maxRankCount

Theorem 6.11

theorem SubsetSum.subset_sum_bound (n k : ℕ) (hk : 0 < k) (S : Finset ℝ) (hScard : S.card = n) (hSpos : ∀ x ∈ S, 0 < x) (α : ℝ) (hα : 0 < α) : subsetSumCount k S α ≤ subsetSumCountNat k n (k * (n + 1) / 2)

Theorem 6.11. Let S be an n-element subset of positive reals, α > 0, and k a positive integer. Then f_k(S, α) ≤ f_k([n], ⌊k(n+1)/2⌋).

Proof. The collection of equal-sum k-subsets of S maps injectively to an antichain in L(k, n-k) via the λ-map (by subsetSumCount_le_maxRankCount, which uses claim_incomparable_of_distinct and Lmn_hasSpernerProperty). The antichain size is bounded by maxRankCount(L(k, n-k)), which equals f_k([n], ⌊k(n+1)/2⌋) by maxRankCount_Lmn_eq.