Skip to content

InformationTheory.Shannon.AEP.Basic.Achievability

Imports 17

Source-coding theorem, achievability #

The source-coding achievability theorem (Cover-Thomas) is stated in Tendsto form. With codebook size M_n := ⌈exp(n · R)⌉, the encoder and decoder are built from a bijection between the typical set and Fin M_n; the error rate vanishes via typicalSet_prob_tendsto_one, and log M_n / n → R follows from a Nat.le_ceil / Nat.ceil_lt_add_one squeeze.

References #

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

noncomputable def

InformationTheory.Shannon.codebookSize

(R : ℝ) (n : ℕ) :

The codebook size used in the achievability proof: M_n := ⌈exp(n · R)⌉.

Equations

InformationTheory.Shannon.codebookSize R n = ⌈Real.exp (↑n * R)⌉₊

Instances For

Used by

theorem

InformationTheory.Shannon.codebookSize_pos

(R : ℝ) (n : ℕ) :

0 < codebookSize R n

Used by

instance

InformationTheory.Shannon.codebookSize_neZero

(R : ℝ) (n : ℕ) :

NeZero (codebookSize R n)

Used by

theorem

InformationTheory.Shannon.typicalSet_card_le_codebookSize

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hpos : ∀ (x : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {x}) (n : ℕ) {ε R : ℝ} (hε : 0 < ε) (h_le : entropy μ (Xs 0) + ε ≤ R) :

⋯.toFinset.card ≤ codebookSize R n

Used by

noncomputable def

InformationTheory.Shannon.aepEncoder

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (n : ℕ) (ε R : ℝ) (h_card_le : ⋯.toFinset.card ≤ codebookSize R n) :

(Fin n → α) → Fin (codebookSize R n)

The encoder: typical blocks → Fin M_n index, non-typical → 0.

Equations

InformationTheory.Shannon.aepEncoder μ Xs n ε R h_card_le x = if hx : x ∈ ⋯.toFinset then Fin.castLE h_card_le (⋯.toFinset.equivFin ⟨x, hx⟩) else ⟨0, ⋯⟩

Instances For

Used by

noncomputable def

InformationTheory.Shannon.aepDecoder

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (n : ℕ) (ε R : ℝ) :

Fin (codebookSize R n) → Fin n → α

The decoder: Fin M_n index → typical block (out of range → default).

Equations

InformationTheory.Shannon.aepDecoder μ Xs n ε R k = if hk : ↑k < ⋯.toFinset.card then ↑(⋯.toFinset.equivFin.symm ⟨↑k, hk⟩) else fun (x : Fin n) => Classical.arbitrary α

Instances For

Used by

theorem

InformationTheory.Shannon.aepDecoder_aepEncoder_of_mem_typicalSet

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (n : ℕ) (ε R : ℝ) (h_card_le : ⋯.toFinset.card ≤ codebookSize R n) (x : Fin n → α) (hx : x ∈ typicalSet μ Xs n ε) :

aepDecoder μ Xs n ε R (aepEncoder μ Xs n ε R h_card_le x) = x

Used by

Error-rate convergence #

theorem

InformationTheory.Shannon.error_subset_compl_typicalSet

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (n : ℕ) (ε R : ℝ) (h_card_le : ⋯.toFinset.card ≤ codebookSize R n) :

{ω : Ω | jointRV Xs n ω ≠ aepDecoder μ Xs n ε R (aepEncoder μ Xs n ε R h_card_le (jointRV Xs n ω))} ⊆ {ω : Ω | jointRV Xs n ω ∉ typicalSet μ Xs n ε}

The error event is contained in {jointRV Xs n ∉ typicalSet}, with the orientation Xs ω ≠ decoder (encoder (Xs ω)) matching errorProb.

Used by

theorem

InformationTheory.Shannon.aep_errorProb_tendsto_zero

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hpos : ∀ (x : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {x}) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) {ε R : ℝ} (hε : 0 < ε) (h_le : entropy μ (Xs 0) + ε ≤ R) :

Filter.Tendsto (fun (n : ℕ) => MeasureFano.errorProb μ (jointRV Xs n) (fun (ω : Ω) => aepEncoder μ Xs n ε R ⋯ (jointRV Xs n ω)) (aepDecoder μ Xs n ε R)) Filter.atTop (nhds 0)

Used by

Rate convergence and achievability theorem #

theorem

InformationTheory.Shannon.codebookSize_log_div_tendsto

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

Filter.Tendsto (fun (n : ℕ) => Real.log ↑(codebookSize R n) / ↑n) Filter.atTop (nhds R)

log M_n / n → R.

Used by

theorem

InformationTheory.Shannon.source_coding_achievability

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hpos : ∀ (x : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {x}) (hindep_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) {R : ℝ} (hR : entropy μ (Xs 0) < R) :

∃ (M : ℕ → ℕ) (_ : ∀ (n : ℕ), 0 < M n) (c : (n : ℕ) → (Fin n → α) → Fin (M n)) (d : (n : ℕ) → Fin (M n) → Fin n → α), Filter.Tendsto (fun (n : ℕ) => Real.log ↑(M n) / ↑n) Filter.atTop (nhds R) ∧ Filter.Tendsto (fun (n : ℕ) => MeasureFano.errorProb μ (jointRV Xs n) (fun (ω : Ω) => c n (jointRV Xs n ω)) (d n)) Filter.atTop (nhds 0)

Source coding theorem (achievability): For any rate R > entropy μ (Xs 0), there exists a block code with rate R and vanishing error.

Used by

Unified source-coding theorem (two-sided equality) #

Combining the weak converse and the achievability direction yields sInf (achievableRates μ Xs) = entropy μ (Xs 0). An "achievable code" is a family (M_n, c_n, d_n) whose error probability vanishes and whose rate log M_n / n is universally bounded (the hM_bdd hypothesis of the converse). The achievability witnesses satisfy this universally-bounded condition because Tendsto rate atTop (𝓝 R) implies BddAbove (Set.range rate) (Filter.Tendsto.bddAbove_range).

structure

InformationTheory.Shannon.IsAchievableCode

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (M : ℕ → ℕ) (c : (n : ℕ) → (Fin n → α) → Fin (M n)) (d : (n : ℕ) → Fin (M n) → Fin n → α) :

An achievable block source code: each M_n > 0, error probability vanishes, and the rate is universally bounded.

hM_pos(n : ℕ) : NeZero (M n)
hPe_to_zero : Filter.Tendsto (fun (n : ℕ) => MeasureFano.errorProb μ (jointRV Xs n) (fun (ω : Ω) => c n (jointRV Xs n ω)) (d n)) Filter.atTop (nhds 0)
hM_bdd : ∃ (R : ℝ), ∀ (n : ℕ), Real.log ↑(M n) / ↑n ≤ R

Instances For

Used by

noncomputable def

InformationTheory.Shannon.achievableRates

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) :

The set of asymptotic rates (liminf log M_n / n) of achievable codes.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.entropy_le_of_mem_achievableRates

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hcard : 2 ≤ Fintype.card α) {r : ℝ} (hr : r ∈ achievableRates μ Xs) :

entropy μ (Xs 0) ≤ r

Every achievable rate is at least the entropy.

Used by

theorem

InformationTheory.Shannon.mem_achievableRates_of_gt_entropy

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hpos : ∀ (x : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {x}) (hindep_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) {R : ℝ} (hR : entropy μ (Xs 0) < R) :

R ∈ achievableRates μ Xs

Any rate strictly above the entropy is achievable.

Used by

theorem

InformationTheory.Shannon.source_coding_theorem

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hpos : ∀ (x : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {x}) (hindep_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hcard : 2 ≤ Fintype.card α) :

sInf (achievableRates μ Xs) = entropy μ (Xs 0)

Source coding theorem: The infimum of asymptotic rates of achievable block source codes equals the entropy of the source.

Used by

Point-wise probability upper bound on the typical set #

For any x ∈ T_ε^n, P^n(x) = ∏ P(x_i) ≤ exp(-n(H - ε)). This is the point-wise companion of the size bound |T_ε^n| ≤ exp(n(H+ε)).

The factorization μ.map (jointRV Xs n) = Measure.pi (μ.map (Xs ·)) requires mutual independence (iIndepFun), not just pairwise independence.

theorem

InformationTheory.Shannon.typicalSet_prob_le

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hpos : ∀ (x : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {x}) (n : ℕ) {ε : ℝ} (x : Fin n → α) (hx : x ∈ typicalSet μ Xs n ε) :

(MeasureTheory.Measure.map (jointRV Xs n) μ).real {x} ≤ Real.exp (-↑n * (entropy μ (Xs 0) - ε))

Point-wise upper bound on typical-set mass: (μ.map (jointRV Xs n)).real {x} ≤ exp(- n · (H - ε)) for any x ∈ T_ε^n.

Used by

Point-wise lower bound and size lower bound #

The remaining two of the four consequences, beyond typicalSet_prob_le (point-wise upper bound), typicalSet_prob_tendsto_one (set probability → 1), and typicalSet_card_le (size upper bound):

typicalSet_prob_ge: point-wise lower bound exp(-n(H+ε)) ≤ P^n(x) for x ∈ T_ε^n
typicalSet_card_ge: size lower bound (1-η) · exp(n(H-ε)) ≤ |T_ε^n| whenever μ(T) ≥ 1-η

theorem

InformationTheory.Shannon.typicalSet_prob_ge

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hpos : ∀ (x : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {x}) (n : ℕ) {ε : ℝ} (x : Fin n → α) (hx : x ∈ typicalSet μ Xs n ε) :

Real.exp (-↑n * (entropy μ (Xs 0) + ε)) ≤ (MeasureTheory.Measure.map (jointRV Xs n) μ).real {x}

Point-wise lower bound on typical-set mass: for x ∈ T_ε^n, exp(-n · (H + ε)) ≤ (μ.map (jointRV Xs n)).real {x}. Dual of typicalSet_prob_le.

Used by

theorem

InformationTheory.Shannon.typicalSet_card_ge

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hpos : ∀ (x : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {x}) (n : ℕ) {ε η : ℝ} (hμ : 1 - η ≤ (MeasureTheory.Measure.map (jointRV Xs n) μ).real (typicalSet μ Xs n ε)) :

(1 - η) * Real.exp (↑n * (entropy μ (Xs 0) - ε)) ≤ ↑⋯.toFinset.card

Size lower bound on typical set: if μ(T_ε^n) ≥ 1 - η, then (1-η) · exp(n · (H - ε)) ≤ |T_ε^n|.

See also typicalSet_prob_tendsto_one.

Used by