Sanov's theorem — type class probability upper bound (A form) #

Cover-Thomas (method of types):

Q^n(T(P)) ≤ exp(-n · D(P‖Q))

where T(P) := { x : Fin n → α | ∀ a, #{i | x i = a} = n · P(a) }.

Main definitions #

• typeCount x a — number of occurrences of a in sequence x : Fin n → α.
• typeClass P n — type class: sequences whose empirical distribution equals P.
• klDivSumForm P Q — finite-alphabet KL sum form: ∑ a, P(a) · (log P(a) - log Q(a)).

Main statements #

• typeClass_Qn_le — Q^n(T(P)) ≤ exp(-n · klDivSumForm P Q).
• klDivSumForm_eq_toReal_klDiv — klDivSumForm P Q = (klDiv P Q).toReal (under absolute continuity).
• typeClass_Qn_le_klDiv — corollary with (klDiv P Q).toReal exponent.

Implementation notes #

• The proof avoids the two-step |T(P)| ≤ exp(n H(P)) + Q^n({x}) = exp(-n(H+D)): it goes directly via Q^n(T) = exp(-n D) · P^n(T) ≤ exp(-n D).
• klDivSumForm is used in the main bound; the equality to (klDiv P Q).toReal is separated into klDivSumForm_eq_toReal_klDiv.

References #

• T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.

Type class definition #

Sanov A main theorem #

(klDiv P Q).toReal form (corollary) #