Formalization of binary symmetric erasure channel based on infotheo
Kyosuke Nakano, Manabu Hagiwara · International Symposium on Information Theory and its Applications · 2016
In this paper, we formalize the channel capacity of the binary symmetric erasure channel (BSEC) by using a proof-assistant system called Coq/SSReflect. This study is for the formalization of the fact that the binary symmetric channel (BSC) and binary erasure channel (BEC), which were previously formalized, are specializations of the BSEC.