InformationTheory.Shannon.ChannelCoding.ConverseMemorylessMarkov

Imports 5

Channel coding converse — strong memoryless DMC variant #

Main definitions #

IsMemorylessChannelStrong: two Markov axioms characterizing a strongly memoryless DMC: per-letter X^n → X_i → Y_i and output conditional independence Y^{≠i} → X^n → Y_i.
measurableEquivExtract i: measurable equivalence Fin n → β ≃ᵐ β × ({j // j ≠ i} → β).

Main statements #

h_markov_xprefix_of_strong: augmented prefix Markov chain from IsMemorylessChannelStrong.
h_split_of_strong: conditional mutual information two-variable chain rule reshape.
channel_coding_converse_general_memoryless_strong: Cover-Thomas converse via entropy subadditivity, yielding log |M| ≤ ∑ I(X_i; Y_i).toReal + Fano.

Implementation notes #

The D-2' hypothesis h_yother_zero : condMI X_i Y^{≠i} (Xprefix, Y_i) = 0 fails for arbitrary encoders (counterexample: n = 2, i = 0, X_1 := X_0). The proof therefore takes the entropy-subadditivity route (mutualInfo_le_sum_per_letter_of_memoryless_strong), which holds for any encoder and bypasses h_yother_zero. The lemmas h_markov_xprefix_of_strong and h_split_of_strong are not called in the main proof but are retained for potential future use.

References #

T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.

Strong memoryless predicate #

structure

InformationTheory.Shannon.ChannelCodingConverseGeneral.IsMemorylessChannelStrong

source

Prop

Strong memoryless DMC predicate (two Markov axioms):

per_letter_markov: for each i, X^n → X_i → Y_i (per-letter channel).
outputs_cond_indep: for each i, Y^{≠i} → X^n → Y_i (outputs conditionally independent given the full input).

per_letter_markov(i : Fin n) : IsMarkovChain μ (fun (ω : Ω) (j : Fin n) => Xs j ω) (Xs i) (Ys i)
Per-letter Markov: Y_i depends on X^n only through X_i.
outputs_cond_indep(i : Fin n) : IsMarkovChain μ (fun (ω : Ω) (j : { j : Fin n // j ≠ i }) => Ys (↑j) ω) (fun (ω : Ω) (j : Fin n) => Xs j ω) (Ys i)
Outputs are conditionally independent across i given the full input X^n.

Instances For

Used by

MeasurableEquiv plumbing #

noncomputable def

InformationTheory.Shannon.ChannelCodingConverseGeneral.measurableEquivExtract

source

{n : ℕ} {β : Type u_2} [MeasurableSpace β] (i : Fin n) :

(Fin n → β) ≃ᵐ β × ({ j : Fin n // j ≠ i } → β)

Fin n → β ≃ᵐ β × ({j : Fin n // j ≠ i} → β): extracts the i-th component and pairs it with the rest.

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

Discharge lemmas #

theorem

InformationTheory.Shannon.ChannelCodingConverseGeneral.h_markov_xprefix_of_strong

source

{Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} {α : Type u_2} [MeasurableSpace α] [Nonempty α] [StandardBorelSpace α] {β : Type u_3} [MeasurableSpace β] [Nonempty β] [StandardBorelSpace β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Fin n → Ω → α) (Ys : Fin n → Ω → β) (hXs : ∀ (i : Fin n), Measurable (Xs i)) (hYs : ∀ (i : Fin n), Measurable (Ys i)) (h_strong : IsMemorylessChannelStrong μ Xs Ys) (i : Fin n) :

IsMarkovChain μ (fun (ω : Ω) => (fun (j : Fin ↑i) => Xs ⟨↑j, ⋯⟩ ω, Xs i ω)) (Xs i) (Ys i)

Augmented prefix Markov chain (X^{<i}, X_i) → X_i → Y_i from IsMemorylessChannelStrong.

Used by

theorem

InformationTheory.Shannon.ChannelCodingConverseGeneral.h_split_of_strong

source

{Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} {α : Type u_2} [MeasurableSpace α] [Nonempty α] [StandardBorelSpace α] {β : Type u_3} [MeasurableSpace β] [Nonempty β] [StandardBorelSpace β] [Fintype α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Fin n → Ω → α) (Ys : Fin n → Ω → β) (hXs : ∀ (i : Fin n), Measurable (Xs i)) (hYs : ∀ (i : Fin n), Measurable (Ys i)) (i : Fin n) :

(condMutualInfo μ (Xs i) (fun (ω : Ω) (j : Fin n) => Ys j ω) fun (ω : Ω) (j : Fin ↑i) => Xs ⟨↑j, ⋯⟩ ω) = (condMutualInfo μ (Xs i) (Ys i) fun (ω : Ω) (j : Fin ↑i) => Xs ⟨↑j, ⋯⟩ ω) + condMutualInfo μ (Xs i) (fun (ω : Ω) (j : { j : Fin n // j ≠ i }) => Ys (↑j) ω) fun (ω : Ω) => (fun (j : Fin ↑i) => Xs ⟨↑j, ⋯⟩ ω, Ys i ω)

Conditional mutual information reshape (independent of memorylessness): condMI X_i Y^n Xprefix = condMI X_i Y_i Xprefix + condMI X_i Y^{≠i} (Xprefix, Y_i).

Used by

Main converse theorem — strong memoryless form #

theorem

InformationTheory.Shannon.ChannelCodingConverseGeneral.channel_coding_converse_general_memoryless_strong

source

{Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} {M : Type u_2} [Fintype M] [Nonempty M] [MeasurableSpace M] [MeasurableSingletonClass M] [StandardBorelSpace M] {α : Type u_3} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [StandardBorelSpace α] {β : Type u_4} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [StandardBorelSpace β] (μ : 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_memo : IsMemorylessChannel μ (fun (i : Fin n) (ω : Ω) => encoder (Msg ω) i) Ys) (h_strong : IsMemorylessChannelStrong μ (fun (i : Fin n) (ω : Ω) => encoder (Msg ω) i) Ys) (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, (mutualInfo μ (fun (ω : Ω) => encoder (Msg ω) i) (Ys i)).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, strong memoryless DMC form): under IsMemorylessChannelStrong, log |M| ≤ ∑ I(X_i; Y_i).toReal + h(Pe) + Pe · log(|M| - 1).

The argument _h_memo : IsMemorylessChannel is unused in the current proof but retained for API compatibility.

Used by