Extremal bound for Katona's intersection theorem

Definition

katonaBound

by xbgxjack · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsextremal-set-theoryintersecting-familieskatona

For natural numbers $n$ and $t$ with $2 \mid (n+t)$ , define

M(n,t) = \sum_{i=(n+t)/2}^{n} \binom{n}{i}.

This is the size of a Hamming ball: viewing subsets of an $n$ -element set as vertices of the $n$ -cube, $M(n,t)$ counts the sets of size at least $(n+t)/2$ , equivalently (via $\binom{n}{i}=\binom{n}{n-i}$ ) the sets within Hamming distance $(n-t)/2$ of the full set $[n]$ . Katona's intersection theorem identifies $M(n,t)$ as the maximum possible size of a $t$ -intersecting family of subsets of $[n]$ , attained by the family of all sets of size at least $(n+t)/2$ .

Definition code

import Mathlib

namespace Katona

/-- The extremal bound in Katona's intersection theorem: the size of a Hamming ball
of the appropriate radius, i.e. the sum of the upper `Finset.Icc ((n + t) / 2) n`
range of binomial coefficients `n.choose i`. -/
noncomputable def katonaBound (n t : ℕ) : ℕ :=
  ∑ i ∈ Finset.Icc ((n + t) / 2) n, n.choose i

end Katona

Source

G. O. H. Katona, Intersection theorems for systems of finite sets, Acta Math. Acad. Sci. Hungar. 15 (1964), 329-337.

View graph