Prove2Me

Sample entropy H‾(xn)\overline{H}(x^n) (Definition 14.2.1)

Definition
WildeQIT_sampleEntropy

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

classical-informationinformation-theorytypicalitywilde-qit

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

Definition 14.2.1 (Sample entropy). The sample entropy H‾(xn)\overline{H}(x^n) of a sequence xnx^n with respect to a probability distribution pX(x)p_X(x) is

H‾(xn)≡−1nlog⁡(pXn(xn)),pXn(xn)=∏i=1npX(xi).\overline{H}(x^n) \equiv -\frac{1}{n}\log\bigl(p_{X^n}(x^n)\bigr), \qquad p_{X^n}(x^n) = \prod_{i=1}^n p_X(x_i).

The sample entropy is the empirical counterpart of H(X)H(X): by the law of large numbers it concentrates around H(X)H(X), which is the origin of typicality.

Formalization Note. WildeQIT.sampleEntropy p x = -(1/n) * Real.logb 2 ((p.iid n).prob x); for n=0n = 0 Lean's 1/0=01/0 = 0 makes it 00, and for a sequence of probability 00 the value is 00 (Real.logb 2 0 = 0) rather than +∞+\infty.

Definition code
import Definitions.Def_WildeQIT_iid
import Definitions.Def_WildeQIT_entropy

/-!
Wilde, *Quantum Information Theory* (2nd ed.), Definition 14.2.1 (Sample entropy):
`H̄(xⁿ) ≡ -(1/n) log p_{Xⁿ}(xⁿ)`, where `p_{Xⁿ}(xⁿ) = ∏ᵢ p_X(xᵢ)`; logarithm base 2.
-/

namespace WildeQIT

/-- Definition 14.2.1. The sample entropy of the sequence `x` with respect to `p`:
`H̄(x) = -(1/n) log₂ (∏ᵢ p(xᵢ))`. -/
noncomputable def sampleEntropy {α : Type} [Fintype α] (p : FinDist α) {n : ℕ} (x : Fin n → α) : ℝ :=
  -(1 / (n : ℝ)) * Real.logb 2 ((p.iid n).prob x)

end WildeQIT
Source
Wilde, Quantum Information Theory 2nd ed. (Cambridge 2017; arXiv:1106.1445v8), Definition 14.2.1, §Weak Typicality (roster-items.csv line 25003).

View graph