module module

`IndisputableMonolith.Information.ChannelCapacity`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (20)

structure Channel L33
structure InputDistribution L49
def mutualInformation L63
theorem mutual_information_nonneg L75
theorem mutual_information_symmetric L81
def channelCapacity L89
theorem mutual_info_bounded L99
theorem uniform_sum_one L143
def uniformDistribution L150
theorem capacity_nonneg L158
theorem shannons_theorem L178
theorem capacity_from_ledger L192
def fundamentalBitRate L202
def bscCapacity L209
def gaussianCapacity L215
theorem gaussian_capacity_increases_with_snr L219
def quantumCapacities L242
theorem holevo_bound L254
def applications L266
structure ChannelCapacityFalsifier L279