InformationTheory.Shannon.SlepianWolf.Achievability

Imports 4

Slepian–Wolf achievability (corner point of the sum bound) #

Starting from the single-shot converse, this file publishes the deterministic achievability of the separate encoder pair (f_X^n, f_Y^n) + d^n at the corner point R_X = log|α|, R_Y > H(Y) (Cover–Thomas).

Main statements #

slepian_wolf_achievability_via_Y_aep — the X-uncompressed, Y-AEP encoder pair: Ys is compressed by a single-source AEP code at any rate R_Y > H(Y) while Xs is sent uncompressed at R_X = log|α|, achieving error → 0. The sum rate R_X + R_Y > log|α| + H(Y) ≥ H(X, Y) covers the segment of the Slepian–Wolf region along the R_X = log|α| boundary.

Implementation notes #

The Y-side AEP code is reused directly from source_coding_achievability. The encoder pair composes the trivial X-encoder f_X := id : (Fin n → α) ≃ Fin (|α|^n) with f_Y := aep_encoder, and the joint decoder is (i, j) ↦ (i_as_xⁿ, aep_decoder j).

Definitions #

noncomputable def

InformationTheory.Shannon.swErrorProb

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} {β : Type u_3} (μ : MeasureTheory.Measure Ω) {n M_X M_Y : ℕ} (Xs : Ω → Fin n → α) (Ys : Ω → Fin n → β) (f_X : (Fin n → α) → Fin M_X) (f_Y : (Fin n → β) → Fin M_Y) (d : Fin M_X × Fin M_Y → (Fin n → α) × (Fin n → β)) :

ℝ

The joint error probability of a Slepian–Wolf encoder pair and joint decoder: the decoder recovers the wrong (x, y) pair.

Equations

InformationTheory.Shannon.swErrorProb μ Xs Ys f_X f_Y d = μ.real {ω : Ω | d (f_X (Xs ω), f_Y (Ys ω)) ≠ (Xs ω, Ys ω)}

Instances For

Used by

Trivial-rate achievability #

noncomputable def

InformationTheory.Shannon.swTrivialEncoderX

source

{α : Type u_2} [Fintype α] (n : ℕ) :

(Fin n → α) → Fin (Fintype.card (Fin n → α))

The trivial Slepian–Wolf X-encoder: the Fintype index of Fin n → α.

Equations

InformationTheory.Shannon.swTrivialEncoderX n = (Fintype.equivFin (Fin n → α)).toFun

Instances For

Used by

noncomputable def

InformationTheory.Shannon.swTrivialEncoderY

source

{β : Type u_3} [Fintype β] (n : ℕ) :

(Fin n → β) → Fin (Fintype.card (Fin n → β))

The trivial Slepian–Wolf Y-encoder: the Fintype index of Fin n → β.

Equations

InformationTheory.Shannon.swTrivialEncoderY n = (Fintype.equivFin (Fin n → β)).toFun

Instances For

Used by

noncomputable def

InformationTheory.Shannon.swTrivialDecoder

source

{α : Type u_2} [Fintype α] {β : Type u_3} [Fintype β] (n : ℕ) :

Fin (Fintype.card (Fin n → α)) × Fin (Fintype.card (Fin n → β)) → (Fin n → α) × (Fin n → β)

The trivial SW joint decoder: apply each axis-equivalence inverse.

Equations

InformationTheory.Shannon.swTrivialDecoder n p = ((Fintype.equivFin (Fin n → α)).invFun p.1, (Fintype.equivFin (Fin n → β)).invFun p.2)

Instances For

Used by

Sum bound via the Y-side AEP encoder #

The X side is sent uncompressed (f_X := identity, M_X := |α|^n) and the Y side is compressed via AEP at any rate R_Y > H(Y) = entropy μ (Ys 0). The joint decoder reads i as the raw Xⁿ (via the trivial inverse) and j as the AEP-decoded Yⁿ.

theorem

InformationTheory.Shannon.slepian_wolf_achievability_via_Y_aep

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {β : Type u_3} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) (hYs : ∀ (i : ℕ), Measurable (Ys i)) (hposY : ∀ (y : β), 0 < (MeasureTheory.Measure.map (Ys 0) μ).real {y}) (hindepY_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Ys i) μ) (hidentY : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Ys i) (Ys 0) μ μ) {R_Y : ℝ} (hR_Y : entropy μ (Ys 0) < R_Y) :

∃ (M_Y : ℕ → ℕ) (_ : ∀ (n : ℕ), 0 < M_Y n) (f_Y : (n : ℕ) → (Fin n → β) → Fin (M_Y n)) (d_Y : (n : ℕ) → Fin (M_Y n) → Fin n → β), Filter.Tendsto (fun (n : ℕ) => Real.log ↑(M_Y n) / ↑n) Filter.atTop (nhds R_Y) ∧ Filter.Tendsto (fun (n : ℕ) => swErrorProb μ (jointRV Xs n) (jointRV Ys n) (swTrivialEncoderX n) (f_Y n) fun (p : Fin (Fintype.card (Fin n → α)) × Fin (M_Y n)) => ((Fintype.equivFin (Fin n → α)).invFun p.1, d_Y n p.2)) Filter.atTop (nhds 0)

The X-uncompressed, Y-AEP encoder pair achieves the corner point (log|α|, R_Y) for any R_Y > H(Y) with errorProb → 0. Given an AEP Y-side encoder/decoder pair (c_Y, d_Y) from source_coding_achievability combined with the trivial X-encoder, the Slepian–Wolf error equals the Y-side AEP error because the X side is decoded perfectly. The sum rate log|α| + R_Y > log|α| + H(Y) ≥ H(X) + H(Y) ≥ H(X, Y).

Used by