Source Coding Theorem

Quentin Hibon and Lawrence C. Paulson

19 October 2016

Abstract

This document contains a proof of the necessary condition on the code rate of a source code, namely that this code rate is bounded by the entropy of the source. This represents one half of Shannon's source coding theorem, which is itself an equivalence.
BSD License

Topics

Theories

Cite

×
@article{Source_Coding_Theorem-AFP,
  author  = {Quentin Hibon and Lawrence C. Paulson},
  title   = {Source Coding Theorem},
  journal = {Archive of Formal Proofs},
  month   = October,
  year    = 2016,
  note    = {\url{http://isa-afp.org/entries/Source_Coding_Theorem.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download