Definitions: Mathlib.InformationTheory

S is a prefix free (from the name)

Let $S$ be an element of the power set of the set of lists of elements of $x$. Then $S$ is a prefix free, if for all lists $x_{1}$ of elements of $x$, if $x_{1}$ is an element of $S$, then for all lists $y$ of elements of $x$, if $y$ is an element of $S$, then if $\operatorname{IsPrefix}$ holds for $x_{1}$ and $y$, then $\EqtMACRoH {x_{1}}{y}$.

Let $S$ be an element of the power set of the set of lists of elements of $x$. Then $\operatorname{IsUniquelyDecodable}$ holds for $S$, if for all lists $x_{1}$ and $x_{2}$ of lists of elements of $x$, if for all lists $w_{1}$ of elements of $x$, if $w_{1}$ is an element of $x_{1}$, then $w_{1}$ is an element of $S$, then if for all lists $w$ of elements of $x$, if $w$ is an element of $x_{2}$, then $w$ is an element of $S$, then if $\EqtMACRoH {\operatorname{flatten} (x_{1})}{\operatorname{flatten} (x_{2})}$, then $\EqtMACRoH {x_{1}}{x_{2}}$.

Let $x_{1}$ be a function from elements of $x$ to sets. Then an element of $\mathrm{Hamming}$ applied to $x_{1}$ is an element of the function that maps $x_{1}$ to the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$.

$\operatorname{ofHamming}$ is an element of $\EquivMACRoAE {\mathrm{Hamming} (x_{1})}{(\mathrm{Elem} (x)\rightarrow x_{1} (i))}$ defined as the identity of $\mathrm{Hamming}$ applied to $x_{1}$.

$\operatorname{toHamming}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow x_{1} (i))}{\mathrm{Hamming} (x_{1})}$ defined as the identity of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$.

Let $x_{4}$ be a function from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$. Let $y$ be a function from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$. Then $\mathrm{hammingDist}$ applied to $i_{1}$, $x_{4}$, $i$ and $y$ is a natural number defined as the function that maps $i$ and $y$ to the cardinality of $\FinsetFilter {i}{\mathrm{Neq} (i_{1} (i), x_{4} (i))}{\FinsetunivMACRoAC}$.

Let $x_{5}$ be a function from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$. Then $\mathrm{hammingNorm}$ applied to $i$ and $x_{5}$ is a natural number defined as the function that maps $x_{5}$ to the cardinality of $\FinsetFilter {i}{\mathrm{Neq} (i (i), 0)}{\FinsetunivMACRoAC}$.

Let $x_{2}$ and $x_{3}$ be measures of $x$. Then $\operatorname{klDiv}$ applied to $x_{2}$ and $x_{3}$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{InformationTheory\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_InformationTheory\_\_KullbackLeibler\_\_Basic\_\_3734523477\_\_\_hygCtx\_\_\_hyg\_\_8}$, $x_{2}$ and $x_{3}$.

the function of x (from the docstring)

Let $x$ be a real number. Then the function of $x$ is a real number defined as the difference between the sum of the product of $x$ and the logarithm of $x$ and $1$ and $x$.