Formalization of entropy measures in HOL

Abstract

Information theory is widely used in a very broad class of scientific and engineering problems, including cryptography, neurobiology, quantum computing, plagiarism detection and other forms of data analysis. Despite the safety-critical nature of some of these applications, most of the information theoretic analysis is done using informal techniques and thus cannot be completely relied upon. To facilitate the formal reasoning about information theoretic aspects, this paper presents a rigorous higher-order logic formalization of some of the most widely used information theoretic principles. Building on fundamental formalizations of measure and Lebesgue integration theories for extended reals, we formalize the Radon-Nikodym derivative and prove some of its properties using the HOL theorem prover. This infrastructure is then used to formalize information theoretic fundamentals like Shannon entropy and relative entropy. We discuss potential applications of the proposed formalization for the analysis of data compression and security protocols. © 2011 Springer-Verlag.