InformationTheory.Shannon.ChannelCoding.ConverseMemorylessChainRule

Imports 6

Channel coding converse (general input) — memoryless per-summand bound #

A memoryless predicate for a discrete memoryless channel together with the conditional mutual-information chain-rule lemmas it needs, used to derive the per-summand inequality of the general-input channel coding converse (Cover–Thomas) from memorylessness alone.

Main definitions #

IsMemorylessChannel μ Xs Ys — a memoryless DMC (without feedback), formalized by the per-time-step Markov chain (X^{≠i}, Y^{≠i}) → X_i → Y_i, i.e. given X_i, the output Y_i is independent of all other inputs and outputs. No explicit channel kernel W is referenced.

Main statements #

condMutualInfo_le_of_markov_joint — under the joint Markov chain (Wc, Xs) → (Wc, Zc) → Yo, I(Xs; Yo | Wc) ≤ I(Zc; Yo | Wc).
condMutualInfo_chain_rule_X_2var / condMutualInfo_chain_rule_Y_2var — two-variable conditional chain rules for condMutualInfo along each axis.

Implementation notes #

The conditional chain-rule lemmas are kept here in local sections rather than in CondMutualInfo.lean, which they leave unmodified; they live in namespace InformationTheory.Shannon, so promoting them to the general API later is easy.

condMutualInfo_le_of_markov_joint does not follow from the bare Markov chain Xs → Zc → Yo alone, since Wc may break that Markov structure; the augmented chain (Wc, Xs) → (Wc, Zc) → Yo is assumed instead, and the common term I(Wc; Yo) is cancelled via the chain rule, which requires I(Wc; Yo) ≠ ∞ (an ENNReal subtraction).

The memoryless-channel predicate #

def

InformationTheory.Shannon.ChannelCodingConverseGeneral.IsMemorylessChannel

source

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

Prop

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

(X^{≠i}, Y^{≠i}) → X_i → Y_i

That is, given X_i, the output Y_i is independent of all other inputs X^{≠i} and all other outputs Y^{≠i}. This captures the textbook memoryless DMC property without referring to an explicit channel kernel W. This is the feedback-free counterpart of IsMemorylessFeedback (no message argument).

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.ChannelCodingConverseGeneral.IsMemorylessChannel.markovChain

source

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

IsMarkovChain μ (fun (ω : Ω) => (fun (j : { j : Fin n // j ≠ i }) => Xs (↑j) ω, fun (j : { j : Fin n // j ≠ i }) => Ys (↑j) ω)) (Xs i) (Ys i)

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

Used by

Conditional mutual-information chain-rule lemmas #

theorem

InformationTheory.Shannon.ChannelCodingConverseGeneral.condMutualInfo_le_of_markov_joint

source

{Ω : Type u_1} [MeasurableSpace Ω] {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {W : Type u_5} [MeasurableSpace X] [StandardBorelSpace X] [Nonempty X] [MeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y] [MeasurableSpace Z] [StandardBorelSpace Z] [Nonempty Z] [MeasurableSpace W] [StandardBorelSpace W] [Nonempty W] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Ω → X) (Zc : Ω → Z) (Yo : Ω → Y) (Wc : Ω → W) (hXs : Measurable Xs) (hZc : Measurable Zc) (hYo : Measurable Yo) (hWc : Measurable Wc) (hmarkov : IsMarkovChain μ (fun (ω : Ω) => (Wc ω, Xs ω)) (fun (ω : Ω) => (Wc ω, Zc ω)) Yo) (hWcYo_fin : mutualInfo μ Wc Yo ≠ ⊤) :

condMutualInfo μ Xs Yo Wc ≤ condMutualInfo μ Zc Yo Wc

Conditional version of mutualInfo_le_of_markov (augmented form).

Under the joint Markov chain (Wc, Xs) → (Wc, Zc) → Yo (i.e., Markov holds with Wc carried on both sides), and assuming I(Wc; Yo) ≠ ∞, we have

I(Xs; Yo | Wc) ≤ I(Zc; Yo | Wc).

This is the natural conditional generalization of mutualInfo_le_of_markov. The single Markov chain Xs → Zc → Yo alone is not sufficient — Wc may break the Markov property unless it is also conditionally compatible, hence the augmented form. The finiteness I(Wc; Yo) ≠ ∞ is needed to cancel the common term after the chain rule.

Used by

theorem

InformationTheory.Shannon.ChannelCodingConverseGeneral.condMutualInfo_chain_rule_X_2var

source

{Ω : Type u_1} [MeasurableSpace Ω] {X : Type u_2} {X' : Type u_3} {Y : Type u_4} {W : Type u_5} [MeasurableSpace X] [StandardBorelSpace X] [Nonempty X] [MeasurableSpace X'] [StandardBorelSpace X'] [Nonempty X'] [MeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y] [MeasurableSpace W] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X_RV : Ω → X) (X'_RV : Ω → X') (Yo : Ω → Y) (Wc : Ω → W) (hX : Measurable X_RV) (hX' : Measurable X'_RV) (hYo : Measurable Yo) (hWc : Measurable Wc) (hWcY_fin : mutualInfo μ Wc Yo ≠ ⊤) :

condMutualInfo μ (fun (ω : Ω) => (X_RV ω, X'_RV ω)) Yo Wc = condMutualInfo μ X_RV Yo Wc + condMutualInfo μ X'_RV Yo fun (ω : Ω) => (Wc ω, X_RV ω)

2-variable X-axis conditional chain rule for condMutualInfo.

I((X, X'); Y | Wc) = I(X; Y | Wc) + I(X'; Y | (Wc, X))

The cancellation of the common term I(Wc; Y) requires I(Wc; Y) ≠ ∞.

Used by

theorem

InformationTheory.Shannon.ChannelCodingConverseGeneral.condMutualInfo_chain_rule_Y_2var

source

{Ω : Type u_1} [MeasurableSpace Ω] {X : Type u_2} {W : Type u_5} [MeasurableSpace X] [StandardBorelSpace X] [Nonempty X] [MeasurableSpace W] {α' : Type u_6} {β' : Type u_7} [MeasurableSpace α'] [StandardBorelSpace α'] [Nonempty α'] [MeasurableSpace β'] [StandardBorelSpace β'] [Nonempty β'] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X_RV : Ω → X) (A : Ω → α') (B : Ω → β') (Wc : Ω → W) (hX : Measurable X_RV) (hA : Measurable A) (hB : Measurable B) (hWc : Measurable Wc) (hWcX_fin : mutualInfo μ Wc X_RV ≠ ⊤) :

condMutualInfo μ X_RV (fun (ω : Ω) => (A ω, B ω)) Wc = condMutualInfo μ X_RV A Wc + condMutualInfo μ X_RV B fun (ω : Ω) => (Wc ω, A ω)

2-variable Y-axis conditional chain rule for condMutualInfo.

I(X; (A, B) | Wc) = I(X; A | Wc) + I(X; B | (Wc, A))

Requires I(Wc; X) ≠ ∞.

Used by