Arithmetic Coding / Shannon-Fano-Elias (Cover-Thomas) #

For a finite-alphabet probability distribution P on α, the arithmetic code assigns each symbol a : α a binary codeword of length ℓ(a) = ⌈-log₂ P(a)⌉ + 1, achieving the expected-length sandwich H₂(P) ≤ E[L] ≤ H₂(P) + 2 and prefix-freeness.

Main definitions #

• sfeLength — Shannon-Fano-Elias codeword length ⌈-log₂ P(a)⌉ + 1.

Main statements #

• sfeLength_kraft_le_one — sfeLength satisfies the Kraft inequality.
• arithmeticCode_expected_length_bounds — H₂(P) ≤ E[L] ≤ H₂(P) + 2.
• arithmeticCode_prefix_free — existence of a length-sfeLength, injective, prefix-free binary code.
• arithmeticCode_unique_decodable — prefix-free ⟹ uniquely decodable.

Implementation notes #

The textbook construction truncates the binary expansion of the cumulative midpoint F̄(a) := F(a) - P(a)/2; the real-valued binary expansion is a Mathlib gap and is avoided entirely. The expected-length bounds use a length-only linear lift of the Shannon-code machinery (entropyD_le_expectedLength_of_kraft / expectedLength_shannon_lt_entropyD_add_one), and the prefix-free code is obtained from exists_prefix_code_of_kraft (integer-slot Kraft-reverse) lifted to List Bool via finTwoEquiv. The textbook midpoint-expansion equivalence is out of scope — it gives the same code and is not needed for the bounds.

References #

• T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006. (Shannon-Fano-Elias coding); (unique decodability).