Lemma 7.6 (Kraft inequality): a prefix-free set S of binary strings has ∑_{σ∈S} 2^{−|σ|} ≤ 1

Proved

UnderstandingML.kraft_inequality

by naimengye · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricskraft-inequalityprefix-free

Lemma 7.6 (Kraft Inequality). If $S \subseteq \{0,1\}^*$ is a prefix-free set of strings, then $\sum_{\sigma \in S} \frac{1}{2^{|\sigma|}} \le 1$ .

Formally: for every finite $F \subseteq S$ , $\sum_{\sigma \in F} (1/2)^{|\sigma|} \le 1$ (equivalent to the series bound, the terms being nonnegative).

Preamble

import Definitions.Def_UnderstandingML_Nonuniform

open MeasureTheory

Formal statement

namespace UnderstandingML

/-- **Lemma 7.6 (Kraft Inequality)** (p. 90). If `S ⊆ {0,1}*` is a prefix-free set of strings,
then `∑_{σ ∈ S} 1/2^{|σ|} ≤ 1` (stated on every finite subfamily, which is the same for a
series of nonnegative terms). -/
theorem kraft_inequality (S : Set (List Bool))
    (hpf : ∀ σ ∈ S, ∀ τ ∈ S, σ ≠ τ → ¬ (σ <+: τ)) :
    ∀ F : Finset (List Bool), ↑F ⊆ S → ∑ σ ∈ F, (1 / 2 : ℝ) ^ σ.length ≤ 1 := by sorry

end UnderstandingML

Source

Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press 2014, doi:10.1017/CBO9781107298019, §7.3 p. 90, Lemma 7.6 with its proof

Human review

Endorsed by Shuze Chen · Sep 25, 2026
Confirmed by the moderator at approval.
Endorsed by naimengye · Sep 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph