InformationTheory.Shannon.ChannelCoding.ConverseGeneral
Channel coding converse — general input form, chain-rule decomposition #
Main statements #
channel_coding_converse_general_chainRule: Without the i.i.d. assumption, the log-cardinality of the message set is bounded by the chain-rule decomposition∑ i, I(X_i; Y^n | X^{<i}).toReal + h(Pe) + Pe · log(|M| - 1).
Implementation notes #
Compared to channel_coding_converse_iid (which collapses I(X^n; Y^n) to
n · I(X_0; Y_0) under the i.i.d. assumption), this form removes the i.i.d.
hypothesis and instead decomposes I(X^n; Y^n) via mutualInfo_chain_rule_fin.
A subsequent per-summand bound I(X_i; Y^n | X^{<i}) ≤ I(X_i; Y_i) (from
memoryless channel properties) would yield Cover-Thomas, but that step is
handled in ConverseMemorylessPure.
InformationTheory.Shannon.channel_coding_converse_general_chainRule
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 : ℕ}
(μ : 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 ω)
(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) ≤ ∑ i : Fin n,
(condMutualInfo μ (fun (ω : Ω) => encoder (Msg ω) i) (fun (ω : Ω) (j : Fin n) => Ys j ω)
fun (ω : Ω) (j : Fin ↑i) => encoder (Msg ω) ⟨↑j, ⋯⟩).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, general chain-rule form):
under a Markov chain Msg → encoder ∘ Msg → Y^n (without any i.i.d. assumption),
log |M| ≤ ∑ i, I(X_i; Y^n | X^{<i}).toReal + h(Pe) + Pe · log(|M| - 1)
where X_i ω := encoder (Msg ω) i, X^{<i} is the prefix RV, and
Pe := errorProb μ Msg Y^n decoder.