InformationTheory.Shannon.RateDistortion.Converse

Imports 8

Rate-distortion converse (single-shot) #

The single-shot form of the rate-distortion converse (Cover–Thomas): R(D̃) ≤ log M for the achieved distortion D̃ := 𝔼 d(X, decoder(encoder X)), obtained from the chain

Real.log M ≥ entropy μ W                    -- MaxEntropy.entropy_le_log_card
          ≥ (mutualInfo μ X W).toReal       -- I = H - H|... ≤ H (condEntropy nonneg)
          ≥ (mutualInfo μ X X̂).toReal       -- DPI: X̂ = decoder ∘ W
          ≥ (rateDistortionFunction P_X D̃).toReal
                                            -- iInf ≤ value at the joint ν := μ.map (X, X̂)

Main definitions #

expectedDistortion — average distortion of a joint distribution.
rateDistortionFunction — the KL-form rate-distortion function.

Main statements #

rate_distortion_converse_single_shot — R(D̃) ≤ log M.

Implementation notes #

The distortion measure is d : α → β → ℝ with no non-negativity assumption. Finiteness of the mutual information is taken as a hypothesis.

References #

T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.

Definitions #

noncomputable def

InformationTheory.Shannon.expectedDistortion

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (d : α → β → ℝ) (ν : MeasureTheory.Measure (α × β)) :

ℝ

Expected distortion of a joint distribution ν : Measure (α × β) under a distortion measure d : α → β → ℝ.

Equations

InformationTheory.Shannon.expectedDistortion d ν = ∫ (p : α × β), d p.1 p.2 ∂ν

Instances For

Used by

noncomputable def

InformationTheory.Shannon.rateDistortionFunction

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (d : α → β → ℝ) (P : MeasureTheory.Measure α) (D : ℝ) :

ENNReal

Rate-distortion function. For a source distribution P : Measure α and distortion threshold D : ℝ, R(D) is the infimum (in ℝ≥0∞) of the joint KL-form mutual information klDiv ν ((ν.map Prod.fst).prod (ν.map Prod.snd)) over feasible joint distributions ν satisfying:

ν.map Prod.fst = P (X-marginal matches source)
expectedDistortion d ν ≤ D (average distortion within threshold)

When no feasible ν exists the iInf is ∞. The value lives in ℝ≥0∞ so the iInf is total.

Equations

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

Instances For

Used by

Basic properties #

theorem

InformationTheory.Shannon.rateDistortionFunction_le_of_feasible

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (d : α → β → ℝ) (P : MeasureTheory.Measure α) (D : ℝ) (ν : MeasureTheory.Measure (α × β)) (hν_marg : MeasureTheory.Measure.map Prod.fst ν = P) (hν_dist : expectedDistortion d ν ≤ D) :

rateDistortionFunction d P D ≤ klDiv ν ((MeasureTheory.Measure.map Prod.fst ν).prod (MeasureTheory.Measure.map Prod.snd ν))

Feasible point ⇒ R(D) ≤ value: exhibiting a feasible joint ν gives an upper bound on the rate-distortion function.

Used by

Single-shot converse #

theorem

InformationTheory.Shannon.rate_distortion_converse_single_shot

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Nonempty α] [MeasurableSingletonClass α] [MeasurableSingletonClass β] {M : Type u_4} [Fintype M] [Nonempty M] [MeasurableSpace M] [MeasurableSingletonClass M] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : Ω → α) (encoder : α → M) (decoder : M → β) (hX : Measurable X) (hencoder : Measurable encoder) (hdecoder : Measurable decoder) (d : α → β → ℝ) (hd : Measurable fun (p : α × β) => d p.1 p.2) (hMI_W_finite : (mutualInfo μ X fun (ω : Ω) => encoder (X ω)) ≠ ⊤) :

(rateDistortionFunction d (MeasureTheory.Measure.map X μ) (∫ (ω : Ω), d (X ω) (decoder (encoder (X ω))) ∂μ)).toReal ≤ Real.log ↑(Fintype.card M)

Rate-distortion theorem (converse, single-shot form).

For any single-shot lossy code (encoder, decoder) with image alphabet M and source random variable X : Ω → α, the rate-distortion function evaluated at the achieved distortion D̃ := 𝔼 d(X, decoder(encoder X)) is bounded above by Real.log |M|:

(rateDistortionFunction d P_X D̃).toReal ≤ Real.log |M|.

Used by