InformationTheory.Shannon.ChannelCoding.FeedbackMemoryless

Imports 6

Feedback channel coding converse — memoryless complete form #

Main definitions #

IsMemorylessFeedback: Per-time-step Markov chain property formalizing a memoryless DMC with causal feedback encoder.

Main statements #

feedback_per_letter_bound: Under IsMemorylessFeedback, the per-letter inequality I(Msg; Y_i | Y^{<i}) ≤ I(X_i; Y_i) holds for all i.
channel_coding_feedback_converse_memoryless: Variant of channel_coding_feedback_converse with h_per_letter replaced by IsMemorylessFeedback.

Implementation notes #

The left RV in IsMemorylessFeedback is (Y^{<i}, Msg) (prefix first, message second), aligning with the chain rule shape mutualInfo μ (fun ω => (Zc ω, Xs ω)) Yo. This avoids a swap step via mutualInfo_map_left_measurableEquiv.

References #

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

Memoryless feedback formalization #

def

InformationTheory.Shannon.ChannelCodingFeedback.IsMemorylessFeedback

source

Prop

A memoryless DMC + causal feedback encoder is formalized by the per-time-step Markov chain property: for each i : Fin n, the random variables form a Markov chain

(Y^{<i}, Msg) → X_i → Y_i

That is, given X_i, the output Y_i is independent of (Y^{<i}, Msg) — which captures both memorylessness (Y_i doesn't depend on Y^{<i}) and causality (Y_i doesn't depend on Msg once X_i is given).

The left RV is (Y^{<i}, Msg) (prefix first, message second), aligning with the chain rule shape mutualInfo μ (fun ω => (Zc ω, Xs ω)) Yo.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.ChannelCodingFeedback.IsMemorylessFeedback.markovChain

source

{Ω : Type u_1} [MeasurableSpace Ω] {M : Type u_2} [MeasurableSpace M] [Nonempty M] [StandardBorelSpace M] {α : Type u_3} [MeasurableSpace α] {β : Type u_4} [MeasurableSpace β] [Nonempty β] [StandardBorelSpace β] {n : ℕ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {Msg : Ω → M} {Xs : Fin n → Ω → α} {Ys : Fin n → Ω → β} (h : IsMemorylessFeedback μ Msg Xs Ys) (i : Fin n) :

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

Accessor: extract the i-th Markov chain from IsMemorylessFeedback.

Used by

Per-letter bound #

theorem

InformationTheory.Shannon.ChannelCodingFeedback.feedback_per_letter_bound

source

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

(condMutualInfo μ Msg (Ys i) fun (ω : Ω) (j : Fin ↑i) => Ys ⟨↑j, ⋯⟩ ω) ≤ mutualInfo μ (Xs i) (Ys i)

Per-letter bound: under IsMemorylessFeedback, I(Msg; Y_i | Y^{<i}) ≤ I(X_i; Y_i) for every i : Fin n.

Used by

Main converse theorem #

theorem

InformationTheory.Shannon.ChannelCodingFeedback.channel_coding_feedback_converse_memoryless

source

{Ω : Type u_1} [MeasurableSpace Ω] {M : Type u_2} [Fintype M] [Nonempty M] [MeasurableSpace M] [MeasurableSingletonClass M] [StandardBorelSpace M] {α : Type u_3} [MeasurableSpace α] {β : Type u_4} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [StandardBorelSpace β] {n : ℕ} (C : ENNReal) (hC_finite : C ≠ ⊤) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Msg : Ω → M) (Xs : Fin n → Ω → α) (Ys : Fin n → Ω → β) (decoder : (Fin n → β) → M) (hMsg : Measurable Msg) (hXs : ∀ (i : Fin n), Measurable (Xs i)) (hYs : ∀ (i : Fin n), Measurable (Ys i)) (hdecoder : Measurable decoder) (h_memo : IsMemorylessFeedback μ Msg Xs Ys) (h_capacity : ∀ (i : Fin n), mutualInfo μ (Xs i) (Ys i) ≤ C) (hMsg_uniform : MeasureTheory.Measure.map Msg μ = (↑(Fintype.card M))⁻¹ • MeasureTheory.Measure.count) (hcard : 2 ≤ Fintype.card M) :

Real.log ↑(Fintype.card M) ≤ ↑n * C.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)

Feedback channel coding theorem (converse, memoryless form).

Variant of channel_coding_feedback_converse with h_per_letter replaced by IsMemorylessFeedback. The per-letter inequality is discharged internally via feedback_per_letter_bound.

Used by