Proposition 8.4.4 — $\sum_{i=0}^n K_t(n,i)\,\tilde x_i(C) \ge 0$

Proved

MatousekLP.Codes.krawtchouk_inequality

by mikedeng1 · Oct 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

coding-theorykrawtchoukp2o-batch-b23bp2o-gran-per-chapterp2o-plan-bookp2o-v1

Let $C \subseteq \{0,1\}^n$ be an arbitrary set of words, let

\tilde x_i = \tilde x_i(C) = \frac{1}{|C|}\bigl|\{(\mathbf w,\mathbf w') \in C^2 : d_H(\mathbf w,\mathbf w') = i\}\bigr|, \qquad i = 0,\dots,n,

and let $t \in \{1,\dots,n\}$ . Then, with the Krawtchouk numbers $K_t(n,i) = \sum_{j=0}^{\min(i,t)}(-1)^j\binom ij\binom{n-i}{t-j}$ ,

\sum_{i=0}^n K_t(n,i)\,\tilde x_i \;\ge\; 0 .

These are exactly the nontrivial constraints of the Delsarte linear program; together with the easy constraints they show that $(\tilde x_0,\dots,\tilde x_n)$ is feasible whenever $C$ is a code with distance $d$ .

Formalization Note $C$ may be empty, in which case Lean's $1/0 = 0$ makes every $\tilde x_i$ zero and the inequality reads $0 \ge 0$ .

Preamble

import Mathlib
import Definitions.Def_MatousekLP_Codes_Basic
import Definitions.Def_MatousekLP_Codes_DelsarteLP

open Finset

Formal statement

namespace MatousekLP.Codes

/-- Proposition 8.4.4, pp. 160–161: for an arbitrary `C ⊆ {0,1}^n` and every
`t ∈ {1, …, n}`, `∑_{i=0}^n K_t(n, i) · x̃_i(C) ≥ 0`. -/
theorem krawtchouk_inequality {n : ℕ} (C : Finset (Word n)) (t : ℕ) (ht1 : 1 ≤ t)
    (htn : t ≤ n) :
    0 ≤ ∑ i ∈ Finset.range (n + 1), (K n t i : ℝ) * xtilde C i := by sorry

end MatousekLP.Codes

Source

Matoušek & Gärtner, Understanding and Using Linear Programming, Springer 2007, pp. 160–161, Proposition 8.4.4

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Proposition 8.4.4 — ∑i=0nKt(n,i) x~i(C)≥0\sum_{i=0}^n K_t(n,i)\,\tilde x_i(C) \ge 0∑i=0n​Kt​(n,i)x~i​(C)≥0

Proposition 8.4.4 — $\sum_{i=0}^n K_t(n,i)\,\tilde x_i(C) \ge 0$