Typical sequences and the typical set $T_\delta^{X^n}$ (Definitions 14.2.2–14.2.3)

Definition

WildeQIT_weakTypicalSet

by aadarwal · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

classical-informationinformation-theorytypicalitywilde-qit

Throughout Chapter 14 an information source emits $n$ independent, identically distributed copies of a random variable $X$ with distribution $p_X$ on a finite alphabet $\mathcal{X}$ ; a realization is a sequence $x^n = x_1\cdots x_n$ (Lean: Fin n → α), with $p_{X^n}(x^n) = \prod_{i=1}^n p_X(x_i)$ . Entropies are in bits.

Definition 14.2.2 (Typical sequence). A sequence $x^n$ is $\delta$ -typical if its sample entropy $\overline{H}(x^n)$ is $\delta$ -close to the entropy $H(X)$ of the random variable $X$ that is the source of the sequence.

Definition 14.2.3 (Typical set). The $\delta$ -typical set $T_\delta^{X^n}$ is the set of all $\delta$ -typical sequences:

T_\delta^{X^n} \equiv \bigl\{ x^n : |\overline{H}(x^n) - H(X)| \le \delta \bigr\}.

Formalization Note. WildeQIT.IsWeakTypical p δ x is the predicate and WildeQIT.weakTypicalSet p n δ : Finset (Fin n → α) the set (a Finset.filter of all sequences); mem_weakTypicalSet unfolds membership.

RETIRED (deprecated) 2026-09-07 03:35. This definition let sequences of probability zero be typical (their sample entropy is 0 under Lean's Real.logb 2 0 = 0, whereas the book's is +∞), so cardinality and equipartition properties stated with it are false. Replaced by WildeQIT_typicalSet (declarations WildeQIT.typicalSet, WildeQIT.IsTypicalSeq) which requires $p_{X^n}(x^n) > 0$ .

Definition code

import Definitions.Def_WildeQIT_sampleEntropy

/-!
Wilde, *Quantum Information Theory* (2nd ed.), Definition 14.2.2 (Typical sequence) and
Definition 14.2.3 (Typical set): a sequence `xⁿ` is `δ`-typical if its sample entropy is
`δ`-close to `H(X)`; the `δ`-typical set is `T_δ^{Xⁿ} ≡ { xⁿ : |H̄(xⁿ) − H(X)| ≤ δ }`.
-/

namespace WildeQIT

variable {α : Type} [Fintype α]

/-- Definition 14.2.2. `x` is a `δ`-typical sequence for the source `p`: `|H̄(x) − H(X)| ≤ δ`. -/
def IsWeakTypical (p : FinDist α) (δ : ℝ) {n : ℕ} (x : Fin n → α) : Prop :=
  |sampleEntropy p x - entropy p| ≤ δ

/-- Definition 14.2.3. The `δ`-typical set `T_δ^{Xⁿ}` of length-`n` sequences. -/
noncomputable def weakTypicalSet (p : FinDist α) (n : ℕ) (δ : ℝ) : Finset (Fin n → α) :=
  Finset.univ.filter fun x => |sampleEntropy p x - entropy p| ≤ δ

theorem mem_weakTypicalSet {p : FinDist α} {n : ℕ} {δ : ℝ} {x : Fin n → α} :
    x ∈ weakTypicalSet p n δ ↔ |sampleEntropy p x - entropy p| ≤ δ := by
  simp [weakTypicalSet]

end WildeQIT

Source

Wilde, Quantum Information Theory 2nd ed. (Cambridge 2017; arXiv:1106.1445v8), Definition 14.2.3, §Weak Typicality, LaTeX label def-ct:weak-typ (roster-items.csv line 25025); and Definition 14.2.2 (Typical Sequence), line 25017.

View graph

Typical sequences and the typical set TδXnT_\delta^{X^n}TδXn​ (Definitions 14.2.2–14.2.3)

Typical sequences and the typical set $T_\delta^{X^n}$ (Definitions 14.2.2–14.2.3)