Source Coding Theorem


Title: Source Coding Theorem
Authors: Quentin Hibon (qh225 /at/ cl /dot/ cam /dot/ ac /dot/ uk) and Lawrence Paulson (lp15 /at/ cam /dot/ ac /dot/ uk)
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.
  author  = {Quentin Hibon and Lawrence Paulson},
  title   = {Source Coding Theorem},
  journal = {Archive of Formal Proofs},
  month   = oct,
  year    = 2016,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License