InformationTheory.Shannon.SlepianWolf.Basic

Imports 10

Slepian–Wolf single-shot converse #

Two sources (Xs, Ys) : Ω → α × β are compressed by independent encoders eX, eY and reconstructed by a joint decoder dec. From an error probability Pe ≤ ε one derives three rate lower bounds:

log Mx        ≥ H(X | Y)   - δ(Pe)
log My        ≥ H(Y | X)   - δ(Pe)
log Mx+log My ≥ H(X, Y)    - δ(Pe)

Main statements #

fano_inequality_with_side_info — Fano with a paired conditioner (Yo, Si).
entropy_ge_condEntropy — conditioning never increases entropy, H(W | Y) ≤ H(W).
slepian_wolf_converse_X / _Y / _sum — the three rate lower bounds.

Fano with side information #

theorem

InformationTheory.Shannon.fano_inequality_with_side_info

source

{Ω : Type u_1} [MeasurableSpace Ω] {X : Type u_2} [Fintype X] [Nonempty X] [MeasurableSpace X] [MeasurableSingletonClass X] {Y : Type u_3} {S : Type u_4} [MeasurableSpace Y] [MeasurableSpace S] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Ω → X) (Yo : Ω → Y) (Si : Ω → S) (decoder : Y × S → X) (hXs : Measurable Xs) (hYo : Measurable Yo) (hSi : Measurable Si) (hdec : Measurable decoder) (hcard : 2 ≤ Fintype.card X) :

(MeasureFano.condEntropy μ Xs fun (ω : Ω) => (Yo ω, Si ω)) ≤ Real.binEntropy (MeasureFano.errorProb μ Xs (fun (ω : Ω) => (Yo ω, Si ω)) decoder) + MeasureFano.errorProb μ Xs (fun (ω : Ω) => (Yo ω, Si ω)) decoder * Real.log (↑(Fintype.card X) - 1)

Fano with side information: condEntropy μ Xs (Yo, Si) ≤ binEntropy(Pe) + Pe · log(|X|-1), with the paired conditioner (Yo, Si).

See also fano_inequality_measure_theoretic.

Used by

Conditioning never increases entropy #

theorem

InformationTheory.Shannon.entropy_ge_condEntropy

source

{Ω : Type u_1} [MeasurableSpace Ω] {W : Type u_2} [Fintype W] [Nonempty W] [MeasurableSpace W] [MeasurableSingletonClass W] {Y : Type u_3} [MeasurableSpace Y] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Ws : Ω → W) (Yo : Ω → Y) (hWs : Measurable Ws) (hYo : Measurable Yo) :

MeasureFano.condEntropy μ Ws Yo ≤ entropy μ Ws

Conditioning never increases entropy: H(W | Y) ≤ H(W).

Used by

The three rate lower bounds #

Each bound chains MaxEntropy.entropy_le_log_card, entropy_ge_condEntropy, a conditional mutual-information bridge, and fano_inequality_with_side_info. The Fano penalty δ(Pe) is written inline as Real.binEntropy Pe + Pe · Real.log (|·| - 1), with the alphabet |α| for the X bound, |β| for the Y bound, and |α × β| for the sum bound.

theorem

InformationTheory.Shannon.slepian_wolf_converse_X

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {β : Type u_3} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] {Mx My : ℕ} [NeZero Mx] [NeZero My] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Ω → α) (Ys : Ω → β) (eX : α → Fin Mx) (eY : β → Fin My) (dec : Fin Mx × Fin My → α × β) (hXs : Measurable Xs) (hYs : Measurable Ys) (hcard : 2 ≤ Fintype.card α) :

Real.log ↑Mx ≥ MeasureFano.condEntropy μ Xs Ys - Real.binEntropy (MeasureFano.errorProb μ Xs (fun (ω : Ω) => (Ys ω, eX (Xs ω))) fun (p : β × Fin Mx) => (dec (p.2, eY p.1)).1) - (MeasureFano.errorProb μ Xs (fun (ω : Ω) => (Ys ω, eX (Xs ω))) fun (p : β × Fin Mx) => (dec (p.2, eY p.1)).1) * Real.log (↑(Fintype.card α) - 1)

Slepian–Wolf converse, X bound: log Mx ≥ H(X | Y) - h(Pe_X) - Pe_X · log(|α| - 1), where Pe_X = μ {ω | Xs ω ≠ decX (Ys ω, eX (Xs ω))} is the marginal X error and decX : β × Fin Mx → α is the X component of the joint decoder, decX(y, m) := (dec(m, eY y)).1.

Used by

theorem

InformationTheory.Shannon.slepian_wolf_converse_Y

source

Real.log ↑My ≥ MeasureFano.condEntropy μ Ys Xs - Real.binEntropy (MeasureFano.errorProb μ Ys (fun (ω : Ω) => (Xs ω, eY (Ys ω))) fun (p : α × Fin My) => (dec (eX p.1, p.2)).2) - (MeasureFano.errorProb μ Ys (fun (ω : Ω) => (Xs ω, eY (Ys ω))) fun (p : α × Fin My) => (dec (eX p.1, p.2)).2) * Real.log (↑(Fintype.card β) - 1)

Slepian–Wolf converse, Y bound (the X/Y-symmetric form): log My ≥ H(Y | X) - h(Pe_Y) - Pe_Y · log(|β| - 1).

Used by

theorem

InformationTheory.Shannon.slepian_wolf_converse_sum

source

Real.log ↑Mx + Real.log ↑My ≥ (entropy μ fun (ω : Ω) => (Xs ω, Ys ω)) - Real.binEntropy (MeasureFano.errorProb μ (fun (ω : Ω) => (Xs ω, Ys ω)) (fun (ω : Ω) => (eX (Xs ω), eY (Ys ω))) dec) - MeasureFano.errorProb μ (fun (ω : Ω) => (Xs ω, Ys ω)) (fun (ω : Ω) => (eX (Xs ω), eY (Ys ω))) dec * Real.log (↑(Fintype.card (α × β)) - 1)

Slepian–Wolf converse, sum bound: log Mx + log My ≥ H(X, Y) - h(Pe) - Pe · log(|α × β| - 1), where Pe = μ {ω | (Xs ω, Ys ω) ≠ dec (eX (Xs ω), eY (Ys ω))} is the joint error.

Used by