InformationTheory

InformationTheory.Shannon.RateDistortion.ConverseMonotone

source

Imports 3

Rate-distortion converse (specified-distortion form) #

The specified-distortion form of the rate-distortion converse (Cover–Thomas):

D̃ := 𝔼 d(X, decoder(encoder X)) ≤ D
⟹ (rateDistortionFunction (μ.map X) D).toReal ≤ Real.log M

Main statements #

Implementation notes #

The specified-distortion bound is the composition of antitonicity of R(D) (D₁ ≤ D₂ ⟹ R(D₂) ≤ R(D₁), from feasible-set inclusion) with the single-shot form R(D̃) ≤ log M, giving R(D) ≤ R(D̃) ≤ log M.

Monotonicity of rateDistortionFunction #

theorem

InformationTheory.Shannon.rateDistortionFunction_antitone

source
{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (d : α → β → ℝ) (P : MeasureTheory.Measure α) {D₁ D₂ : ℝ} (hD : D₁ ≤ D₂) :
rateDistortionFunction d P D₂ ≤ rateDistortionFunction d P D₁

The rate-distortion function is antitone in the distortion threshold: enlarging the feasibility budget can only lower the infimum.

Used by

    Specified-distortion single-shot converse #

    theorem

    InformationTheory.Shannon.rate_distortion_converse_single_shot_specified

    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 ω)) ≠ ⊤) {D : ℝ} (hD : ∫ (ω : Ω), d (X ω) (decoder (encoder (X ω))) ∂μ ≤ D) :
    (rateDistortionFunction d (MeasureTheory.Measure.map X μ) D).toReal ≤ Real.log ↑(Fintype.card M)

    Rate-distortion theorem (converse, specified-distortion form).

    For any single-shot lossy code (encoder, decoder) with image alphabet M and source random variable X : Ω → α, if the actual expected distortion D̃ := 𝔼 d(X, decoder(encoder X)) does not exceed a specified threshold D, then the rate-distortion function at the specified threshold D is also bounded by Real.log |M|:

    ∫ ω, d (X ω) (decoder (encoder (X ω))) ∂μ ≤ D
⟹ (rateDistortionFunction d (μ.map X) D).toReal ≤ Real.log |M|.

    This is the form most commonly seen in textbooks (R(D) ≤ rate).

    Used by