Formalization of the variable-length source coding theorem: Direct part. - Ryosuke Obi; Manabu Hagiwara; Reynald Affeldt (ISITA, 2014)