InformationTheory.Shannon.RateDistortion.AchievabilityCodebookMatchProbability

Imports 3

Rate-distortion achievability — codebook-level match probability #

Lower bounds on the probability that some codeword of an i.i.d. product codebook is jointly typical with a source word, and the source-averaged failure probability obtained by integrating over the source distribution.

Main statements #

codebook_indep_no_match_prob_eq — under the product measure Measure.pi (fun _ : Fin M => p), the probability that no codeword matches x factors as (1 - p.real {y | (x, y) ∈ JTS}) ^ M.
single_codeword_typical_match_prob — the probability that some codeword matches x is at least 1 - (1 - p.real {y | (x, y) ∈ JTS}) ^ M.
encoder_failure_prob_le_exp_neg_M_avg — exponentialization of the source-averaged failure-pow bound.

Source-averaged failure probability #

Integrating the per-source-word bound single_codeword_typical_match_prob over the source distribution P_X produces a bound on the source-averaged failure probability. The non-trivial step is the Fubini-style bridge rewriting ∫ x, p.real {y | (x, y) ∈ JTS} ∂P_X as (P_X.prod p).real (JTS).

theorem

InformationTheory.Shannon.one_sub_pow_le_exp_neg_mul

source

(M : ℕ) {t : ℝ} (_h0 : 0 ≤ t) (h1 : t ≤ 1) :

(1 - t) ^ M ≤ Real.exp (-↑M * t)

Utility: (1 - t)^M ≤ exp (-M·t) for 0 ≤ t ≤ 1. Used to convert the per-codeword no-match probability into an exponential bound.

Used by

theorem

InformationTheory.Shannon.encoder_failure_prob_le_exp_neg_M_avg

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) {M n : ℕ} (ε : ℝ) (P_X : MeasureTheory.Measure (Fin n → α)) [MeasureTheory.IsProbabilityMeasure P_X] (p : MeasureTheory.Measure (Fin n → β)) [MeasureTheory.IsProbabilityMeasure p] :

∫ (x : Fin n → α), (1 - p.real {y : Fin n → β | (x, y) ∈ ChannelCoding.jointlyTypicalSet μ Xs Ys n ε}) ^ M ∂P_X ≤ ∫ (x : Fin n → α), Real.exp (-↑M * p.real {y : Fin n → β | (x, y) ∈ ChannelCoding.jointlyTypicalSet μ Xs Ys n ε}) ∂P_X

Exponentialization of the source-averaged failure-pow bound. Pointwise (1 - p_typ x)^M ≤ exp(-M · p_typ x), then integrate.

Used by

Pigeonhole (existence from average) #

A Codebook M n β-indexed function whose codebookMeasure-weighted average is ≤ B admits at least one deterministic codebook attaining ≤ B. Verbatim mirror of ChannelCodingAchievability.exists_codebook_le_avg, but stated generically over a function f : Codebook M n β → ℝ so it serves both the channel-coding-style and lossy-distortion-style consumers.

theorem

InformationTheory.Shannon.exists_codebook_low_avg

source

{β : Type u_3} [MeasurableSpace β] [Fintype β] [Nonempty β] [MeasurableSingletonClass β] {M n : ℕ} (p : MeasureTheory.Measure β) [MeasureTheory.IsProbabilityMeasure p] (f : ChannelCoding.Codebook M n β → ℝ) {B : ℝ} (h_avg : ∑ c : ChannelCoding.Codebook M n β, (ChannelCoding.codebookMeasure p M n).real {c} * f c ≤ B) :

∃ (c : ChannelCoding.Codebook M n β), f c ≤ B

Pigeonhole (probabilistic-method form, lossy version). If a real-valued codebook functional has codebookMeasure-weighted average ≤ B, then some deterministic codebook achieves f c ≤ B.

Stated for a codebook over the reconstruction alphabet β; verbatim mirror of ChannelCodingAchievability.exists_codebook_le_avg, but free of the codebookToCode / averageErrorProb plumbing so it can wrap either the channel-coding error functional or the lossy-distortion functional.

Used by