InformationTheory.Shannon.RateDistortion.AchievabilityAsymptoticFailureDecay

Imports 4

Rate-distortion achievability — asymptotic decay and distortion decomposition #

The asymptotic part of the rate-distortion achievability argument: from the per-n bounds (joint-typicality probability ≥ (1-η)·exp(-n·θ), codebook size M_n ≥ ⌈exp(n·R)⌉, and the source-averaged failure bound (1 - p_typ)^M ≤ exp(-M · p_typ)), the random-coding failure probability tends to 0 provided R > θ ≥ 0. Also provides the distortion decomposition of the joint-typical encoder into the within-δ and worst-case branches.

Main definitions #

distortionMax d — the worst-case single-letter distortion, an absolute upper bound on blockDistortion.

Main statements #

ceil_exp_mul_exp_neg_tendsto_atTop — M_n · exp(-nθ) → ∞ when R > θ.
exp_neg_tendsto_zero_of_tendsto_atTop — f n → ∞ ⟹ exp(-f n) → 0.
blockDistortion_le_distortionMax — blockDistortion ≤ distortionMax.
source_avg_distortion_le_simpler — codebook-fixed Bochner-integral form of the distortion decomposition: ∫ x, blockDistortion ∂P_X is bounded by (𝔼d + δ) + distortionMax · Pr(encoder fails distortion-typicality).

theorem

InformationTheory.Shannon.ceil_exp_mul_exp_neg_tendsto_atTop

source

{R θ : ℝ} (hRθ : θ < R) :

Filter.Tendsto (fun (n : ℕ) => ↑⌈Real.exp (↑n * R)⌉₊ * Real.exp (-↑n * θ)) Filter.atTop Filter.atTop

M_n · exp(-nθ) → ∞ when M_n ≥ ⌈exp(nR)⌉ and R > θ.

Used by

theorem

InformationTheory.Shannon.exp_neg_tendsto_zero_of_tendsto_atTop

source

{f : ℕ → ℝ} (hf : Filter.Tendsto f Filter.atTop Filter.atTop) :

Filter.Tendsto (fun (n : ℕ) => Real.exp (-f n)) Filter.atTop (nhds 0)

exp(-f n) → 0 when f n → ∞.

Used by

Distortion decomposition #

noncomputable def

InformationTheory.Shannon.distortionMax

source

{α : Type u_2} {β : Type u_3} [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] (d : DistortionFn α β) :

ℝ

The maximum single-letter distortion over the (finite, nonempty) alphabet α × β, taken as a real number. Used as the worst-case bound for blockDistortion on the encoder-fail event.

Equations

InformationTheory.Shannon.distortionMax d = Finset.univ.sup' ⋯ fun (ab : α × β) => ↑(d ab.1 ab.2)

Instances For

Used by

theorem

InformationTheory.Shannon.distortionMax_nonneg

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSingletonClass β] (d : DistortionFn α β) :

0 ≤ distortionMax d

distortionMax is non-negative.

Used by

theorem

InformationTheory.Shannon.distortion_le_distortionMax

source

↑(d a b) ≤ distortionMax d

Per-symbol bound: each ((d a b : NNReal) : ℝ) ≤ distortionMax d.

Used by

theorem

InformationTheory.Shannon.blockDistortion_le_distortionMax

source

blockDistortion d n x y ≤ distortionMax d

blockDistortion d n x y ≤ distortionMax d.

Used by

theorem

InformationTheory.Shannon.expectedJointDistortion_nonneg

source

0 ≤ expectedJointDistortion μ X Y d

expectedJointDistortion is non-negative (integrand is NNReal-valued).

Used by

theorem

InformationTheory.Shannon.integral_const_add_indicator_one

source

{S : Type u_4} [MeasurableSpace S] (P : MeasureTheory.Measure S) [MeasureTheory.IsProbabilityMeasure P] (B : Set S) (hB : MeasurableSet B) (a m : ℝ) :

∫ (x : S), a + m * B.indicator (fun (x : S) => 1) x ∂P = a + m * P.real B

For a probability measure P on S, integrating a + m · 1_B yields a + m · P.real B.

Used by

theorem

InformationTheory.Shannon.source_avg_distortion_le_simpler

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) (d : DistortionFn α β) {M n : ℕ} (hM : 0 < M) (ε : ℝ) {δ : ℝ} (hδ : 0 ≤ δ) (c : ChannelCoding.Codebook M n β) (P_X : MeasureTheory.Measure (Fin n → α)) [MeasureTheory.IsProbabilityMeasure P_X] :

∫ (x : Fin n → α), blockDistortion d n x (c (jointTypicalLossyEncoder μ Xs Ys hM ε c x)) ∂P_X ≤ expectedJointDistortion μ (Xs 0) (Ys 0) d + δ + distortionMax d * P_X.real {x : Fin n → α | (x, c (jointTypicalLossyEncoder μ Xs Ys hM ε c x)) ∉ distortionTypicalSet μ Xs Ys d n ε δ}

Codebook-fixed average distortion decomposition.

For a fixed deterministic codebook c : Codebook M n β and the joint-typical lossy encoder, the source-averaged block distortion satisfies

∫ x, blockDistortion d n x (c (encoder x)) ∂P_X
  ≤ (𝔼[d(X_0, Y_0)] + δ)
    + distortionMax d
      · P_X { x | (x, c (encoder x)) ∉ distortionTypicalSet }

The failure event is stated encoder-side: the encoder's chosen codeword is not distortion-typical. The hypothesis hδ : 0 ≤ δ ensures 𝔼[d] + δ ≥ 0, simplifying the decomposition dMax ≤ (𝔼[d] + δ) + dMax * 1.

Used by