InformationTheory.Shannon.ChannelCoding.Feedback

Imports 7

Channel coding feedback converse — chain-rule form #

Cover-Thomas: for a DMC with feedback, capacity equals the memoryless capacity. The per-letter inequality I(M; Y_i | Y^{<i}) ≤ I(X_i; Y_i) is left as a hypothesis h_per_letter; its internal proof is in FeedbackComplete.

Main definitions #

FeedbackCode M n α β: feedback code structure with causal encoder encoder : ∀ i : Fin n, Fin M → (Fin i.val → β) → α.

Main statements #

mutualInfo_chain_rule_Y_axis_fin: Y-axis n-variable chain rule I(M; Y^n) = ∑ I(M; Y_i | Y^{<i}).
channel_coding_feedback_converse_chain: Under the per-letter bound hypothesis, I(M; Y^n) ≤ ∑ I(X_i; Y_i).
channel_coding_feedback_converse_capacity: Under I(X_i; Y_i) ≤ C for all i, I(M; Y^n) ≤ n • C.
channel_coding_feedback_converse: Combines Fano inequality with the above to give log |M| ≤ n · C + h(Pe) + Pe · log(|M| - 1).

References #

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

`FeedbackCode` structure #

structure

InformationTheory.Shannon.ChannelCodingFeedback.FeedbackCode

source

(M n : ℕ) (α : Type u_2) (β : Type u_3) :

Type (max u_2 u_3)

A feedback code of length n with M messages. The encoder at time i takes the message and the prior outputs Y_0, …, Y_{i-1} to produce the input symbol X_i ∈ α. The decoder maps the full output block Y^n to a message guess.

X_i = encoder i m (y_0, …, y_{i-1}) — the causal structure is built into the type signature: encoder i : Fin M → (Fin i.val → β) → α only sees Fin i.val → β.

encoder(i : Fin n) : Fin M → (Fin ↑i → β) → α
decoder : (Fin n → β) → Fin M

Instances For

Used by

def

InformationTheory.Shannon.ChannelCodingFeedback.FeedbackCode.decodingRegion

source

{M n : ℕ} {α : Type u_2} {β : Type u_3} (c : FeedbackCode M n α β) (m : Fin M) :

Set (Fin n → β)

The decoding region for message m.

Equations

c.decodingRegion m = {y : Fin n → β | c.decoder y = m}

Instances For

Used by

def

InformationTheory.Shannon.ChannelCodingFeedback.FeedbackCode.errorEvent

source

{M n : ℕ} {α : Type u_2} {β : Type u_3} (c : FeedbackCode M n α β) (m : Fin M) :

Set (Fin n → β)

The error event for message m.

Equations

c.errorEvent m = (c.decodingRegion m)ᶜ

Instances For

Used by

def

InformationTheory.Shannon.ChannelCodingFeedback.FeedbackCode.ofCode

source

{M n : ℕ} {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (c : ChannelCoding.Code M n α β) :

FeedbackCode M n α β

A degenerate feedback encoder is one whose encoder i ignores its (Fin i.val → β) input. Equivalently: a standard Code (no feedback). The achievability statement C_FB ≥ C is trivially captured by the embedding of Code into FeedbackCode via this degenerate construction.

Equations

InformationTheory.Shannon.ChannelCodingFeedback.FeedbackCode.ofCode c = { encoder := fun (i : Fin n) (m : Fin M) (x : Fin ↑i → β) => c.encoder m i, decoder := c.decoder }

Instances For

Used by

theorem

InformationTheory.Shannon.ChannelCodingFeedback.FeedbackCode.ofCode_decoder

source

@[simp]

{M n : ℕ} {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (c : ChannelCoding.Code M n α β) :

(ofCode c).decoder = c.decoder

Used by

theorem

InformationTheory.Shannon.ChannelCodingFeedback.FeedbackCode.ofCode_encoder

source

@[simp]

{M n : ℕ} {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (c : ChannelCoding.Code M n α β) (i : Fin n) (m : Fin M) (yprev : Fin ↑i → β) :

(ofCode c).encoder i m yprev = c.encoder m i

Used by

theorem

InformationTheory.Shannon.ChannelCodingFeedback.FeedbackCode.ofCode_decodingRegion

source

@[simp]

{M n : ℕ} {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (c : ChannelCoding.Code M n α β) (m : Fin M) :

(ofCode c).decodingRegion m = c.decodingRegion m

Used by

theorem

InformationTheory.Shannon.ChannelCodingFeedback.FeedbackCode.ofCode_errorEvent

source

@[simp]

{M n : ℕ} {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (c : ChannelCoding.Code M n α β) (m : Fin M) :

(ofCode c).errorEvent m = c.errorEvent m

Used by

Y-axis n-variable chain rule #

theorem

InformationTheory.Shannon.ChannelCodingFeedback.mutualInfo_chain_rule_Y_axis_fin

source

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

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

Y-axis n-variable chain rule for mutual information: I(Msg; Y_0, …, Y_{n-1}) = ∑ i, I(Msg; Y_i | (Y_0, …, Y_{i-1})).

Used by

Chain-rule converse (hypothesis form) #

theorem

InformationTheory.Shannon.ChannelCodingFeedback.channel_coding_feedback_converse_chain

source

{Ω : Type u_1} [MeasurableSpace Ω] {M : Type u_2} [MeasurableSpace M] [Nonempty M] [StandardBorelSpace M] {α : Type u_3} [MeasurableSpace α] {β : Type u_4} [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] [Nonempty β] [StandardBorelSpace β] {n : ℕ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Msg : Ω → M) (Xs : Fin n → Ω → α) (Ys : Fin n → Ω → β) (hMsg : Measurable Msg) (hYs : ∀ (i : Fin n), Measurable (Ys i)) (h_per_letter : ∀ (i : Fin n), (condMutualInfo μ Msg (Ys i) fun (ω : Ω) (j : Fin ↑i) => Ys ⟨↑j, ⋯⟩ ω) ≤ mutualInfo μ (Xs i) (Ys i)) :

(mutualInfo μ Msg fun (ω : Ω) (i : Fin n) => Ys i ω) ≤ ∑ i : Fin n, mutualInfo μ (Xs i) (Ys i)

Chain-rule converse (chain step, hypothesis form): under the per-letter bound I(Msg; Y_i | Y^{<i}) ≤ I(X_i; Y_i), I(Msg; Y^n) ≤ ∑ i, I(X_i; Y_i).

@audit:retract-candidate(superseded-by-memoryless-form)

Used by

theorem

InformationTheory.Shannon.ChannelCodingFeedback.channel_coding_feedback_converse_capacity

source

{Ω : Type u_1} [MeasurableSpace Ω] {M : Type u_2} [MeasurableSpace M] [Nonempty M] [StandardBorelSpace M] {α : Type u_3} [MeasurableSpace α] {β : Type u_4} [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] [Nonempty β] [StandardBorelSpace β] {n : ℕ} (C : ENNReal) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Msg : Ω → M) (Xs : Fin n → Ω → α) (Ys : Fin n → Ω → β) (hMsg : Measurable Msg) (hYs : ∀ (i : Fin n), Measurable (Ys i)) (h_per_letter : ∀ (i : Fin n), (condMutualInfo μ Msg (Ys i) fun (ω : Ω) (j : Fin ↑i) => Ys ⟨↑j, ⋯⟩ ω) ≤ mutualInfo μ (Xs i) (Ys i)) (h_capacity : ∀ (i : Fin n), mutualInfo μ (Xs i) (Ys i) ≤ C) :

(mutualInfo μ Msg fun (ω : Ω) (i : Fin n) => Ys i ω) ≤ n • C

Capacity upper bound (hypothesis form): per-letter bound + I(X_i; Y_i) ≤ C for all i implies I(Msg; Y^n) ≤ n • C (where n • C is nsmul in ℝ≥0∞).

@audit:retract-candidate(superseded-by-memoryless-form)

Used by

Main converse theorem #

theorem

InformationTheory.Shannon.ChannelCodingFeedback.channel_coding_feedback_converse

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) (hYs : ∀ (i : Fin n), Measurable (Ys i)) (hdecoder : Measurable decoder) (h_per_letter : ∀ (i : Fin n), (condMutualInfo μ Msg (Ys i) fun (ω : Ω) (j : Fin ↑i) => Ys ⟨↑j, ⋯⟩ ω) ≤ mutualInfo μ (Xs i) (Ys i)) (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 converse, hypothesis form.

Under the per-letter bound I(Msg; Y_i | Y^{<i}) ≤ I(X_i; Y_i) and I(X_i; Y_i) ≤ C for all i, combined with the Fano inequality:

log |M| ≤ n · C.toReal + h(Pe) + Pe · log(|M| - 1)

where Pe := μ {Msg ≠ decoder ∘ Y^n}. The capacity C is an arbitrary ℝ≥0∞ value; callers supply the DMC capacity bound. Unlike channel_coding_converse_iid, no Markov chain on Msg → encoder ∘ Msg → Y^n is required (feedback breaks it).

@audit:retract-candidate(superseded-by-memoryless-form)

Used by

InformationTheory.Shannon.ChannelCoding.Feedback

Channel coding feedback converse — chain-rule form #

Main definitions #

Main statements #

References #

FeedbackCode structure #

Y-axis n-variable chain rule #

Chain-rule converse (hypothesis form) #

Main converse theorem #

`FeedbackCode` structure #