InformationTheory.Shannon.BlockwiseChannel.CapacityLimit
Blockwise channel capacity: the asymptotic limit form #
For memoryless DMC, the asymptotic per-letter capacity
capacity_lim W := lim_{n → ∞} (1/n) · sup_{p^n} I(X^n; Y^n) matches the
single-letter capacity W. This follows directly from the per-n equality
capacityN_ofMemoryless_eq (the sequence is eventually the constant
capacity W).
Main statements #
capacity_lim_eq_capacity_of_memoryless— the limit form matches the single-letter capacity.
InformationTheory.Shannon.ChannelCoding.capacity_lim_eq_capacity_of_memoryless
source{α : Type u_1}
{β : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[StandardBorelSpace α]
[Fintype β]
[Nonempty β]
[MeasurableSpace β]
[MeasurableSingletonClass β]
[StandardBorelSpace β]
(W : Channel α β)
[ProbabilityTheory.IsMarkovKernel W]
:
Limit form matches the single-letter capacity W in the memoryless case.
Direct from the per-n equality (the sequence is eventually the constant
capacity W).