InformationTheory.Shannon.ChannelCoding.Converse
Channel coding converse — n-variable i.i.d. form #
Main statements #
channel_coding_converse_iid: Under a Markov chainMsg → encoder ∘ Msg → Y^nand an i.i.d. joint distribution assumption, the log-cardinality of the message set is bounded byn · I(X_0; Y_0) + h(Pe) + Pe · log(|M| - 1).
InformationTheory.Shannon.channel_coding_converse_iid
source{Ω : Type u_1}
[MeasurableSpace Ω]
{M : Type u_2}
[Fintype M]
[Nonempty M]
[MeasurableSpace M]
[MeasurableSingletonClass M]
{α : Type u_3}
{β : Type u_4}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype β]
[Nonempty β]
[MeasurableSpace β]
[MeasurableSingletonClass β]
{n : ℕ}
(hn : 0 < n)
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Msg : Ω → M)
(encoder : M → Fin n → α)
(Ys : Fin n → Ω → β)
(decoder : (Fin n → β) → M)
(hMsg : Measurable Msg)
(hYs : ∀ (i : Fin n), Measurable (Ys i))
(hdecoder : Measurable decoder)
(hmarkov : IsMarkovChain μ Msg (fun (ω : Ω) => encoder (Msg ω)) fun (ω : Ω) (i : Fin n) => Ys i ω)
(h_iid_joint :
MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => (encoder (Msg ω) i, Ys i ω)) μ = MeasureTheory.Measure.pi fun (i : Fin n) =>
MeasureTheory.Measure.map (fun (ω : Ω) => (encoder (Msg ω) i, Ys i ω)) μ)
(h_iid_X :
MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => encoder (Msg ω) i) μ = MeasureTheory.Measure.pi fun (i : Fin n) => MeasureTheory.Measure.map (fun (ω : Ω) => encoder (Msg ω) i) μ)
(h_iid_Y :
MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => Ys i ω) μ = MeasureTheory.Measure.pi fun (i : Fin n) => MeasureTheory.Measure.map (Ys i) μ)
(h_copy :
∀ (i : Fin n),
MeasureTheory.Measure.map (fun (ω : Ω) => (encoder (Msg ω) i, Ys i ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (encoder (Msg ω) ⟨0, hn⟩, Ys ⟨0, hn⟩ ω)) μ)
(h_copy_X :
∀ (i : Fin n),
MeasureTheory.Measure.map (fun (ω : Ω) => encoder (Msg ω) i) μ = MeasureTheory.Measure.map (fun (ω : Ω) => encoder (Msg ω) ⟨0, hn⟩) μ)
(h_copy_Y : ∀ (i : Fin n), MeasureTheory.Measure.map (Ys i) μ = MeasureTheory.Measure.map (Ys ⟨0, hn⟩) μ)
(hMsg_uniform : MeasureTheory.Measure.map Msg μ = (↑(Fintype.card M))⁻¹ • MeasureTheory.Measure.count)
(hcard : 2 ≤ Fintype.card M)
(hMI_finite : (mutualInfo μ (fun (ω : Ω) => encoder (Msg ω)) fun (ω : Ω) (i : Fin n) => Ys i ω) ≠ ⊤)
:
Real.log ↑(Fintype.card M) ≤ ↑n * (mutualInfo μ (fun (ω : Ω) => encoder (Msg ω) ⟨0, hn⟩) (Ys ⟨0, hn⟩)).toReal + Real.binEntropy (MeasureFano.errorProb μ Msg (fun (ω : Ω) (i : Fin n) => Ys i ω) decoder) + MeasureFano.errorProb μ Msg (fun (ω : Ω) (i : Fin n) => Ys i ω) decoder * Real.log (↑(Fintype.card M) - 1)
Shannon's noisy channel coding theorem (converse, n-letter i.i.d. form):
under a Markov chain Msg → encoder ∘ Msg → Y^n and an i.i.d. joint
distribution assumption,
log |M| ≤ n · I(X_0; Y_0).toReal + h(Pe) + Pe · log(|M| - 1)
where X_0 ω := encoder (Msg ω) 0, Y_0 := Ys 0, and
Pe := errorProb μ Msg Y^n decoder.