InformationTheory.Shannon.ChannelCoding.ShannonTheoremMaxError
Shannon noisy channel coding theorem — max-error achievability (umbrella) #
Umbrella module for the max-error form of the Shannon noisy channel coding theorem. Supporting lemmas are split into part files:
ShannonTheoremMaxError/SeedLemmas.lean— smooth input distribution and capacity lower bound construction.ShannonTheoremMaxError/PmfLogBounds.lean— closed-form pmfLog variance bounds.ShannonTheoremMaxError/SmoothInstantiation.lean— achievability at the smooth channel with explicitNformula.ShannonTheoremMaxError/OuterN.lean— outerNconstruction combining TV bound and smooth achievability.
This file contains only the main theorem
shannon_noisy_channel_coding_theorem_general.
Main theorem #
InformationTheory.Shannon.ChannelCoding.shannon_noisy_channel_coding_theorem_general
source{α : Type u_1}
{β : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype β]
[Nonempty β]
[MeasurableSpace β]
[MeasurableSingletonClass β]
(W : Channel α β)
[ProbabilityTheory.IsMarkovKernel W]
{R : ℝ}
(hR_pos : 0 < R)
(hR : R < capacity W)
{ε : ℝ}
(hε : 0 < ε)
:
Shannon's noisy channel coding theorem (general, max-error form): for R < capacity W
and any ε > 0, there exists N such that for all n ≥ N there is a code with
M ≥ ⌈exp(nR)⌉ codewords achieving max-error less than ε.