InformationTheory.Shannon.WynerZiv.Basic

Imports 4

Wyner–Ziv lossy distributed coding #

The rate-distortion function for Wyner–Ziv lossy compression with side information Y available at the decoder only (Cover–Thomas):

R_WZ(D) = min_{p(u|x), f : U × Y → X̂} [ I(X ; U) − I(Y ; U) ]

with the minimization subject to the Markov chain U − X − Y and the distortion constraint 𝔼 d(X, f(U, Y)) ≤ D.

This file defines the WynerZivCode structure, the joint pmf marginals, the WynerZivConstraint feasible set, the wynerZivRatePmf rate function, the slice-attainment lemma, and the rate-equality wrapper wyner_ziv_tendsto. The achievability and converse legs are developed in WynerZiv/Achievability.lean and WynerZiv/Converse.lean.

Main definitions #

WynerZivCode — a Wyner–Ziv block code (X-side encoder, side-information decoder).
wzMarginalXY, wzMarginalXU, wzMarginalYU — the marginals of a joint pmf.
WynerZivConstraint — the feasible (q, f) pairs.
wynerZivRatePmf — the rate function R_WZ(D).

Main statements #

continuous_wzObjective — continuity of the objective I(X;U) − I(Y;U).
wynerZivRatePmf_attained_slice — the objective attains its minimum on a decoder slice.
wyner_ziv_tendsto — the rate-equality form from two-sided bounds.

Implementation notes #

The decoder f : U × β → γ is carried as an external second component, so the constraint set lives on (α × β × U → ℝ) × (U × β → γ). The auxiliary alphabet U is taken as an argument rather than constructed from a cardinality bound.

Wyner–Ziv block code #

structure

InformationTheory.Shannon.WynerZivCode

source

(M n : ℕ) (α : Type u_1) (β : Type u_2) (γ : Type u_3) [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] :

Type (max (max u_1 u_2) u_3)

A Wyner–Ziv block code of length n with M codewords. Encoder is X-side only; decoder takes (codeword, side info Y^n) and reproduces an estimate of X^n over the reconstruction alphabet γ.

encoder : (Fin n → α) → Fin M
decoder : Fin M × (Fin n → β) → Fin n → γ

Instances For

Used by

noncomputable def

InformationTheory.Shannon.WynerZivCode.expectedBlockDistortion

source

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {M n : ℕ} (c : WynerZivCode M n α β γ) (P_XY : MeasureTheory.Measure (α × β)) (d : DistortionFn α γ) :

ℝ

Expected block distortion of a Wyner–Ziv code under a joint source measure P_XY on α × β. The source is i.i.d., so (X^n, Y^n) is distributed according to Measure.pi (fun _ => P_XY) on (α × β)^n.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.WynerZivCode.expectedBlockDistortion_nonneg

source

0 ≤ c.expectedBlockDistortion P_XY d

Expected block distortion is non-negative (the integrand is a non-negative real-valued function).

Used by

pmf form: 3-variable marginals and mutual informations #

noncomputable def

InformationTheory.Shannon.wzMarginalXY

source

{α : Type u_1} {β : Type u_2} (U : Type u_3) [Fintype U] (q : α × β × U → ℝ) :

α × β → ℝ

(α, β)-marginal of a joint pmf q : α × β × U → ℝ.

Equations

InformationTheory.Shannon.wzMarginalXY U q p = ∑ u : U, q (p.1, p.2, u)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.wzMarginalXU

source

{α : Type u_1} {β : Type u_2} [Fintype β] (U : Type u_3) (q : α × β × U → ℝ) :

α × U → ℝ

(α, U)-marginal of a joint pmf q : α × β × U → ℝ.

Equations

InformationTheory.Shannon.wzMarginalXU U q p = ∑ y : β, q (p.1, y, p.2)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.wzMarginalYU

source

{α : Type u_1} {β : Type u_2} [Fintype α] (U : Type u_3) (q : α × β × U → ℝ) :

β × U → ℝ

(β, U)-marginal of a joint pmf q : α × β × U → ℝ.

Equations

InformationTheory.Shannon.wzMarginalYU U q p = ∑ x : α, q (x, p.1, p.2)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.wzMutualInfoXU

source

{α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (U : Type u_3) [Fintype U] (q : α × β × U → ℝ) :

ℝ

3-variable mutual information I(X ; U) for a joint pmf q : α × β × U → ℝ, defined as mutualInfoPmf (wzMarginalXU q).

Equations

InformationTheory.Shannon.wzMutualInfoXU U q = InformationTheory.Shannon.mutualInfoPmf (InformationTheory.Shannon.wzMarginalXU U q)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.wzMutualInfoYU

source

{α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (U : Type u_3) [Fintype U] (q : α × β × U → ℝ) :

ℝ

3-variable mutual information I(Y ; U) for a joint pmf q : α × β × U → ℝ, defined as mutualInfoPmf (wzMarginalYU q).

Equations

InformationTheory.Shannon.wzMutualInfoYU U q = InformationTheory.Shannon.mutualInfoPmf (InformationTheory.Shannon.wzMarginalYU U q)

Instances For

Used by

theorem

InformationTheory.Shannon.continuous_wzMarginalXY

source

{α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_3) [Fintype U] [MeasurableSpace U] :

Continuous fun (q : α × β × U → ℝ) => wzMarginalXY U q

wzMarginalXY is continuous in q (finite sum of evaluations).

Used by

theorem

InformationTheory.Shannon.continuous_wzMarginalXU

source

{α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_3) [Fintype U] [MeasurableSpace U] :

Continuous fun (q : α × β × U → ℝ) => wzMarginalXU U q

wzMarginalXU is continuous in q.

Used by

theorem

InformationTheory.Shannon.continuous_wzMarginalYU

source

{α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_3) [Fintype U] [MeasurableSpace U] :

Continuous fun (q : α × β × U → ℝ) => wzMarginalYU U q

wzMarginalYU is continuous in q.

Used by

theorem

InformationTheory.Shannon.continuous_wzMutualInfoXU

source

{α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_3) [Fintype U] [MeasurableSpace U] :

Continuous fun (q : α × β × U → ℝ) => wzMutualInfoXU U q

wzMutualInfoXU is continuous in q.

Used by

theorem

InformationTheory.Shannon.continuous_wzMutualInfoYU

source

{α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_3) [Fintype U] [MeasurableSpace U] :

Continuous fun (q : α × β × U → ℝ) => wzMutualInfoYU U q

wzMutualInfoYU is continuous in q.

Used by

theorem

InformationTheory.Shannon.continuous_wzObjective

source

{α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_3) [Fintype U] [MeasurableSpace U] :

Continuous fun (q : α × β × U → ℝ) => wzMutualInfoXU U q - wzMutualInfoYU U q

The Wyner–Ziv objective I(X ; U) − I(Y ; U) is continuous in the joint pmf.

Used by

Wyner–Ziv constraint set #

The decoder f : U × β → γ is carried as an external second component, so the constraint set lives on the product (α × β × U → ℝ) × (U × β → γ). The Markov constraint U − X − Y is encoded in cross-product form, well-defined even where marginals vanish (inventory).

noncomputable def

InformationTheory.Shannon.wzExpectedDistortion

source

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] (U : Type u_4) [Fintype U] (d : α → γ → ℝ) (q : α × β × U → ℝ) (f : U × β → γ) :

ℝ

Distortion functional in pmf form for Wyner–Ziv: ∑_{x,y,u} q(x,y,u) · d(x, f(u,y)).

Equations

InformationTheory.Shannon.wzExpectedDistortion U d q f = ∑ p : α × β × U, q p * d p.1 (f (p.2.2, p.2.1))

Instances For

Used by

def

InformationTheory.Shannon.wzMarkovCrossEq

source

{α : Type u_1} {β : Type u_2} [Fintype β] (U : Type u_4) (q : α × β × U → ℝ) :

Prop

Markov-chain cross-product form q(x,y,u) · q_X(x,u') = q(x,y,u') · q_X(x,u) where q_X(x,u) := ∑_y q(x,y,u). Encoded as a real-valued affine condition (well-defined where q_X vanishes — both sides become 0).

Equations

InformationTheory.Shannon.wzMarkovCrossEq U q = ∀ (x : α) (y : β) (u u' : U), q (x, y, u) * ∑ y' : β, q (x, y', u') = q (x, y, u') * ∑ y' : β, q (x, y', u)

Instances For

Used by

def

InformationTheory.Shannon.WynerZivConstraint

source

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] (U : Type u_4) [Fintype U] (P_XY : α × β → ℝ) (d : α → γ → ℝ) (D : ℝ) :

Set ((α × β × U → ℝ) × (U × β → γ))

Wyner–Ziv constraint set — feasible (q, f) pairs satisfying:

q ∈ stdSimplex ℝ (α × β × U) — non-negative pmf with total mass 1.
wzMarginalXY q = P_XY — (X, Y) marginal matches the source.
wzMarkovCrossEq q — Markov chain U − X − Y.
wzExpectedDistortion d q f ≤ D — expected distortion within budget.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.mem_WynerZivConstraint_iff

source

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_4) [Fintype U] [MeasurableSpace U] {P_XY : α × β → ℝ} {d : α → γ → ℝ} {D : ℝ} {qf : (α × β × U → ℝ) × (U × β → γ)} :

qf ∈ WynerZivConstraint U P_XY d D ↔ qf.1 ∈ stdSimplex ℝ (α × β × U) ∧ wzMarginalXY U qf.1 = P_XY ∧ wzMarkovCrossEq U qf.1 ∧ wzExpectedDistortion U d qf.1 qf.2 ≤ D

Membership unfold for WynerZivConstraint.

Used by

Wyner–Ziv rate function #

noncomputable def

InformationTheory.Shannon.wynerZivRatePmf

source

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] (U : Type u_4) [Fintype U] (P_XY : α × β → ℝ) (d : α → γ → ℝ) (D : ℝ) :

ℝ

The Wyner–Ziv rate function (pmf form), R_WZ(D) := sInf { I(X;U) − I(Y;U) | (q, f) ∈ WynerZivConstraint U P_XY d D }, with the auxiliary alphabet U taken as an argument.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.wynerZivRatePmf_le_of_feasible

source

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_4) [Fintype U] [MeasurableSpace U] (P_XY : α × β → ℝ) (d : α → γ → ℝ) (D : ℝ) (qf : (α × β × U → ℝ) × (U × β → γ)) (hqf : qf ∈ WynerZivConstraint U P_XY d D) (h_bdd : BddBelow ((fun (qf : (α × β × U → ℝ) × (U × β → γ)) => wzMutualInfoXU U qf.1 - wzMutualInfoYU U qf.1) '' WynerZivConstraint U P_XY d D)) :

wynerZivRatePmf U P_XY d D ≤ wzMutualInfoXU U qf.1 - wzMutualInfoYU U qf.1

Upper bound from any feasible point: if (q, f) ∈ WynerZivConstraint and the image is bounded below (which it always is on the simplex), then wynerZivRatePmf ≤ I(X;U)(q) − I(Y;U)(q).

Used by

theorem

InformationTheory.Shannon.wynerZivRatePmf_attained_slice

source

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_4) [Fintype U] [MeasurableSpace U] (P_XY : α × β → ℝ) (d : α → γ → ℝ) (D : ℝ) (f₀ : U × β → γ) (h_ne : {q : α × β × U → ℝ | (q, f₀) ∈ WynerZivConstraint U P_XY d D}.Nonempty) :

∃ qStar ∈ {q : α × β × U → ℝ | (q, f₀) ∈ WynerZivConstraint U P_XY d D}, IsMinOn (fun (q : α × β × U → ℝ) => wzMutualInfoXU U q - wzMutualInfoYU U q) {q : α × β × U → ℝ | (q, f₀) ∈ WynerZivConstraint U P_XY d D} qStar

Attainment (slice form) — fix a decoder f₀ : U × β → γ and assume the slice K f₀ := {q | (q, f₀) ∈ WynerZivConstraint U P_XY d D} is non-empty. Then there exists a qStar ∈ K f₀ minimizing the Wyner–Ziv objective I(X;U) − I(Y;U) over K f₀. This is the structural ingredient that the achievability/converse proofs rely on; the full joint attainment over (q, f) requires further hypotheses on (γ, U, β) and is deferred.

Used by

theorem

InformationTheory.Shannon.wynerZivRatePmf_image_bddBelow_of_objective

source

BddBelow ((fun (qf : (α × β × U → ℝ) × (U × β → γ)) => wzMutualInfoXU U qf.1 - wzMutualInfoYU U qf.1) '' WynerZivConstraint U P_XY d D)

The image of the Wyner–Ziv constraint set under the objective is bounded below by any caller-supplied lower bound B (the canonical bound is -Real.log (Fintype.card U), since I(X;U) ≥ 0 and I(Y;U) ≤ Real.log (Fintype.card U) on a finite alphabet).

Used by

Rate-equality wrapper #

theorem

InformationTheory.Shannon.wyner_ziv_tendsto

source

R = wynerZivRatePmf U P_XY d D

Wyner–Ziv theorem (rate-equality form): from achievability R ≥ wynerZivRatePmf(D) and converse R ≤ wynerZivRatePmf(D), R = wynerZivRatePmf(D). The two-sided hypotheses are discharged in WynerZiv/Achievability.lean and WynerZiv/Converse.lean.

Used by