InformationTheory.Shannon.WynerZiv.Operational

Imports 5

Wyner–Ziv operational achievability predicate #

This file provides the operational-achievability predicate WynerZivAchievable shared by the Wyner–Ziv converse and achievability legs, together with the single-letter pmf-to-measure bridge relating the pmf-form mutual informations wzMutualInfoXU / wzMutualInfoYU to the measure-form mutualInfo.

Main definitions #

WynerZivAchievable — a rate R is achievable at distortion D for the i.i.d. source P_XY if there is a sequence of Wyner–Ziv block codes whose log-cardinality rate tends to R and whose expected block distortion is eventually within D + ε for every ε > 0.

Main statements #

wzMutualInfoXU_eq_mutualInfo — the pmf-form I(X;U) of the joint pmf induced by a measure equals the measure-form (mutualInfo μ X U).toReal.
wzMutualInfoYU_eq_mutualInfo — the analogous identity for I(Y;U).

Implementation notes #

The distortion component of WynerZivAchievable uses the distortion-only "eventually within D + ε" form (equivalently limsup ≤ D), matching the distortion-only rate-distortion achievability/converse templates (rate_distortion_achievability, rate_distortion_converse_single_shot); the WynerZivCode structure exposes no codeword, so no error-probability component is bundled here — error probability is an achievability-internal device deferred to the achievability leg. The predicate is a pure existential with the two limit conditions; no proof core is carried inside it.

Operational achievability predicate #

def

InformationTheory.Shannon.WynerZivAchievable

source

{α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (P_XY : MeasureTheory.Measure (α × β)) (d : DistortionFn α γ) (R D : ℝ) :

Prop

A rate R is Wyner–Ziv achievable at distortion D for the i.i.d. source P_XY on α × β (side information Y at the decoder only) if there is a sequence of Wyner–Ziv block codes c n : WynerZivCode (M n) n α β γ such that:

the log-cardinality rate log (M n) / n tends to R, and
for every ε > 0, the expected block distortion of c n is eventually (in n) within D + ε.

The distortion condition is the distortion-only "eventually ≤ D + ε" form (equivalently limsup ≤ D). This is a pure existential over code sequences plus the two limit conditions; no proof content is carried in the predicate. @audit:ok

Equations

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

Instances For

Used by

pmf-to-measure bridge for the single-letter mutual informations #

The bridge relates the pmf-form wzMutualInfoXU/wzMutualInfoYU (finite-sum negMulLog form of I(X;U)/I(Y;U)) of the empirical joint pmf induced by a measure to the measure-form mutualInfo. Internally it factors through a fully general two-variable identity mutualInfoPmf_empirical_eq_mutualInfo plus a marginalization of the three-variable empirical pmf down to a two-variable one.

theorem

InformationTheory.Shannon.wzMutualInfoXU_eq_mutualInfo

source

{α : Type u_1} {β : Type u_2} {U : Type u_4} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [Fintype U] [Nonempty U] [MeasurableSpace U] [MeasurableSingletonClass U] {Ω : Type u_5} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : Ω → α) (Y : Ω → β) (Uc : Ω → U) (hX : Measurable X) (hY : Measurable Y) (hU : Measurable Uc) :

(wzMutualInfoXU U fun (p : α × β × U) => (MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, Y ω, Uc ω)) μ).real {p}) = (mutualInfo μ X Uc).toReal

The pmf-form mutual information I(X;U) of the three-variable joint pmf induced by a probability measure μ with coordinates X, Y, U equals the measure-form (mutualInfo μ X U).toReal. Stated in .toReal form so it composes with the single-letterization of the converse leg.

Used by

theorem

InformationTheory.Shannon.wzMutualInfoYU_eq_mutualInfo

source

(wzMutualInfoYU U fun (p : α × β × U) => (MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, Y ω, Uc ω)) μ).real {p}) = (mutualInfo μ Y Uc).toReal

The pmf-form mutual information I(Y;U) of the three-variable joint pmf induced by a probability measure μ with coordinates X, Y, U equals the measure-form (mutualInfo μ Y U).toReal. Stated in .toReal form so it composes with the single-letterization of the converse leg.

Used by