InformationTheory

InformationTheory.Shannon.Converse

source

Imports 9

Single-shot Shannon channel coding converse #

The converse to the channel coding theorem (single-shot version): for a uniformly distributed message Msg and channel output Yo, log |M| ≤ I(Msg; Yo) + h(Pe) + Pe · log(|M| - 1).

Main statements #

Implementation notes #

The proof chains entropy μ Msg = log |M| (uniform), the Bridge identity mutualInfo_eq_entropy_sub_condEntropy, the DPI mutualInfo_le_of_postprocess (applied to decoder : Y → M), and the Fano inequality. The encoder-free formulation is adopted because I(Msg; Yo) ≤ I(encoder ∘ Msg; Yo) does not hold without a Markov assumption; the Markov-encoder corollary is proved separately.

theorem

InformationTheory.Shannon.shannon_converse_single_shot

source
{Ω : Type u_1} [MeasurableSpace Ω] {M : Type u_2} [Fintype M] [Nonempty M] [MeasurableSpace M] [MeasurableSingletonClass M] {Y : Type u_3} [MeasurableSpace Y] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Msg : Ω → M) (Yo : Ω → Y) (decoder : Y → M) (hMsg : Measurable Msg) (hYo : Measurable Yo) (hdecoder : Measurable decoder) (hMsg_uniform : MeasureTheory.Measure.map Msg μ = (↑(Fintype.card M))⁻¹ • MeasureTheory.Measure.count) (hcard : 2 ≤ Fintype.card M) (hMI_finite : mutualInfo μ Msg Yo ≠ ⊤) :
Real.log ↑(Fintype.card M) ≤ (mutualInfo μ Msg Yo).toReal + Real.binEntropy (MeasureFano.errorProb μ Msg Yo decoder) + MeasureFano.errorProb μ Msg Yo decoder * Real.log (↑(Fintype.card M) - 1)

The single-shot converse to the channel coding theorem: for a uniformly distributed message Msg transmitted via channel output Yo and decoded by decoder, log |M| ≤ I(Msg; Yo) + h(Pe) + Pe · log(|M| - 1), where Pe = errorProb μ Msg Yo decoder = μ {Msg ≠ decoder ∘ Yo}.

Requires mutualInfo μ Msg Yo ≠ ∞ so that .toReal is monotone across DPI.

Used by

    Corollary: injective encoder #

    For an injective encoder : M → X, one additional application of the DPI with decoder' := Function.invFun encoder gives I(Msg; Yo) ≤ I(encoder ∘ Msg; Yo), which combines with shannon_converse_single_shot to give the encoder-included bound.

    Corollary: Markov encoder #

    theorem

    InformationTheory.Shannon.shannon_converse_single_shot_markov_encoder

    source
    {Ω : Type u_1} [MeasurableSpace Ω] {M : Type u_2} [Fintype M] [Nonempty M] [MeasurableSpace M] [MeasurableSingletonClass M] {Y : Type u_3} [MeasurableSpace Y] {X : Type u_4} [MeasurableSpace X] [StandardBorelSpace X] [Nonempty X] [StandardBorelSpace Y] [Nonempty Y] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Msg : Ω → M) (encoder : M → X) (Yo : Ω → Y) (decoder : Y → M) (hMsg : Measurable Msg) (hYo : Measurable Yo) (hencoder : Measurable encoder) (hdecoder : Measurable decoder) (hmarkov : IsMarkovChain μ Msg (encoder ∘ Msg) Yo) (hMsg_uniform : MeasureTheory.Measure.map Msg μ = (↑(Fintype.card M))⁻¹ • MeasureTheory.Measure.count) (hcard : 2 ≤ Fintype.card M) (hMI_finite : mutualInfo μ (encoder ∘ Msg) Yo ≠ ⊤) :
    Real.log ↑(Fintype.card M) ≤ (mutualInfo μ (encoder ∘ Msg) Yo).toReal + Real.binEntropy (MeasureFano.errorProb μ Msg Yo decoder) + MeasureFano.errorProb μ Msg Yo decoder * Real.log (↑(Fintype.card M) - 1)

    Single-shot Shannon converse with a Markov encoder: under the Markov chain Msg → encoder ∘ Msg → Yo, log |M| ≤ I(encoder ∘ Msg; Yo) + h(Pe) + Pe · log(|M| - 1).

    Used by