# Source Coding Theorem

 Title: Source Coding Theorem Authors: Quentin Hibon (qh225 /at/ cl /dot/ cam /dot/ ac /dot/ uk) and Lawrence C. Paulson Submission date: 2016-10-19 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. BibTeX: @article{Source_Coding_Theorem-AFP, author = {Quentin Hibon and Lawrence C. Paulson}, title = {Source Coding Theorem}, journal = {Archive of Formal Proofs}, month = oct, year = 2016, note = {\url{http://isa-afp.org/entries/Source_Coding_Theorem.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.