Skip to content

InformationTheory.Shannon.Stein.Achievability

Imports 9

Stein's lemma: achievability #

Stein's lemma for binary hypothesis testing (Cover–Thomas): the optimal type-II error of an n-sample test with type-I error at most ε decays exponentially in n at the rate of the Kullback–Leibler divergence klDiv P Q. This file develops the achievability (lower bound) side: the log-likelihood-ratio plumbing, the Stein-typical set, and the tensorization of the KL divergence.

Main definitions #

llrPmf P Q — the alphabet-side log-likelihood ratio log P{x} − log Q{x}.
logLikelihoodRatio P Q Xs i — the per-sample log-likelihood ratio along a process Xs.
steinTypicalSet P Q n ε — blocks whose empirical log-likelihood ratio is within ε of klDiv P Q.

Main statements #

stein_strong_law — the empirical mean of the log-likelihood ratio converges almost surely to (klDiv P Q).toReal.
stein_inProbability — the same convergence holds in probability.
stein_achievability — there exist ε-level tests whose type-II error decays at rate klDiv P Q.

Implementation notes #

The log-likelihood-ratio plumbing is obtained as the two-distribution specialization of the AEP development, which lets most measurability, identical-distribution, and independence lemmas be reused rather than reproved.
Over a finite alphabet α with 0 < Q.real {x} for every x, all quantities are expanded point-wise, avoiding the general Radon–Nikodym derivative machinery for product measures.

References #

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

Log-likelihood ratio plumbing #

noncomputable def

InformationTheory.Shannon.llrPmf

{α : Type u_2} [MeasurableSpace α] (P Q : MeasureTheory.Measure α) :

α → ℝ

The alphabet-side log-likelihood ratio log P{x} − log Q{x}. On the support of P and assuming Q{x} > 0 for all x, this equals Real.log ((P.rnDeriv Q x).toReal).

Equations

InformationTheory.Shannon.llrPmf P Q x = Real.log (P.real {x}) - Real.log (Q.real {x})

Instances For

Used by

theorem

InformationTheory.Shannon.measurable_llrPmf

{α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : MeasureTheory.Measure α) :

Measurable (llrPmf P Q)

Used by

noncomputable def

InformationTheory.Shannon.logLikelihoodRatio

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

Ω → ℝ

Per-symbol log-likelihood ratio: llrPmf P Q (Xs i ω).

Equations

InformationTheory.Shannon.logLikelihoodRatio P Q Xs i ω = InformationTheory.Shannon.llrPmf P Q (Xs i ω)

Instances For

Used by

theorem

InformationTheory.Shannon.logLikelihoodRatio_eq_comp

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

logLikelihoodRatio P Q Xs i = llrPmf P Q ∘ Xs i

Used by

theorem

InformationTheory.Shannon.measurable_logLikelihoodRatio

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : MeasureTheory.Measure α) (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (i : ℕ) :

Measurable (logLikelihoodRatio P Q Xs i)

Used by

theorem

InformationTheory.Shannon.integrable_logLikelihoodRatio

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P Q : MeasureTheory.Measure α) (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (i : ℕ) :

MeasureTheory.Integrable (logLikelihoodRatio P Q Xs i) μ

Used by

theorem

InformationTheory.Shannon.integral_logLikelihoodRatio_under_P

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hMap : MeasureTheory.Measure.map (Xs 0) μ = P) (hPQ : P.AbsolutelyContinuous Q) (hQpos : ∀ (x : α), 0 < Q.real {x}) :

∫ (ω : Ω), logLikelihoodRatio P Q Xs 0 ω ∂μ = (klDiv P Q).toReal

The expected log-likelihood ratio under P equals (klDiv P Q).toReal.

Used by

theorem

InformationTheory.Shannon.identDistrib_logLikelihoodRatio

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) (P Q : MeasureTheory.Measure α) (Xs : ℕ → Ω → α) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (i : ℕ) :

ProbabilityTheory.IdentDistrib (logLikelihoodRatio P Q Xs i) (logLikelihoodRatio P Q Xs 0) μ μ

Used by

theorem

InformationTheory.Shannon.indepFun_logLikelihoodRatio

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) (P Q : MeasureTheory.Measure α) (Xs : ℕ → Ω → α) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ) :

Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (logLikelihoodRatio P Q Xs i) (logLikelihoodRatio P Q Xs j) μ

Used by

theorem

InformationTheory.Shannon.stein_strong_law

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hMap : MeasureTheory.Measure.map (Xs 0) μ = P) (hPQ : P.AbsolutelyContinuous Q) (hQpos : ∀ (x : α), 0 < Q.real {x}) :

∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => (∑ i ∈ Finset.range n, logLikelihoodRatio P Q Xs i ω) / ↑n) Filter.atTop (nhds (klDiv P Q).toReal)

The empirical mean of the per-sample log-likelihood ratio converges almost surely to (klDiv P Q).toReal.

Used by

theorem

InformationTheory.Shannon.stein_inProbability

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hMap : MeasureTheory.Measure.map (Xs 0) μ = P) (hPQ : P.AbsolutelyContinuous Q) (hQpos : ∀ (x : α), 0 < Q.real {x}) {ε : ℝ} (hε : 0 < ε) :

Filter.Tendsto (fun (n : ℕ) => μ {ω : Ω | ε ≤ |(∑ i ∈ Finset.range n, logLikelihoodRatio P Q Xs i ω) / ↑n - (klDiv P Q).toReal|}) Filter.atTop (nhds 0)

The empirical mean of the log-likelihood ratio converges to (klDiv P Q).toReal in probability.

Used by

Stein-typical set and achievability #

noncomputable def

InformationTheory.Shannon.steinTypicalSet

{α : Type u_2} [MeasurableSpace α] (P Q : MeasureTheory.Measure α) (n : ℕ) (ε : ℝ) :

Set (Fin n → α)

The Stein-typical set: blocks x : Fin n → α whose empirical log-likelihood ratio is within ε of (klDiv P Q).toReal.

Equations

InformationTheory.Shannon.steinTypicalSet P Q n ε = {x : Fin n → α | |(∑ i : Fin n, InformationTheory.Shannon.llrPmf P Q (x i)) / ↑n - (InformationTheory.klDiv P Q).toReal| < ε}

Instances For

Used by

theorem

InformationTheory.Shannon.mem_steinTypicalSet_iff

{α : Type u_2} [MeasurableSpace α] (P Q : MeasureTheory.Measure α) (n : ℕ) (ε : ℝ) (x : Fin n → α) :

x ∈ steinTypicalSet P Q n ε ↔ |(∑ i : Fin n, llrPmf P Q (x i)) / ↑n - (klDiv P Q).toReal| < ε

Used by

theorem

InformationTheory.Shannon.measurableSet_steinTypicalSet

{α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : MeasureTheory.Measure α) (n : ℕ) (ε : ℝ) :

MeasurableSet (steinTypicalSet P Q n ε)

Used by

theorem

InformationTheory.Shannon.steinTypicalSet_P_prob_tendsto_one

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hMap : MeasureTheory.Measure.map (Xs 0) μ = P) (hPQ : P.AbsolutelyContinuous Q) (hQpos : ∀ (x : α), 0 < Q.real {x}) {ε : ℝ} (hε : 0 < ε) :

Filter.Tendsto (fun (n : ℕ) => μ {ω : Ω | jointRV Xs n ω ∈ steinTypicalSet P Q n ε}) Filter.atTop (nhds 1)

Under P, the probability that a block lands in the Stein-typical set tends to 1.

Used by

theorem

InformationTheory.Shannon.steinTypicalSet_Q_prob_le

{α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (hPpos : ∀ (x : α), 0 < P.real {x}) (hQpos : ∀ (x : α), 0 < Q.real {x}) (n : ℕ) (ε : ℝ) :

((MeasureTheory.Measure.pi fun (x : Fin n) => Q) (steinTypicalSet P Q n ε)).toReal ≤ Real.exp (-(↑n * ((klDiv P Q).toReal - ε)))

The Qⁿ-mass of the Stein-typical set is at most exp(-n · ((klDiv P Q).toReal − ε)).

Used by

theorem

InformationTheory.Shannon.stein_achievability

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (P Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hMap : MeasureTheory.Measure.map (Xs 0) μ = P) (hMapJoint : ∀ (n : ℕ), MeasureTheory.Measure.map (jointRV Xs n) μ = MeasureTheory.Measure.pi fun (x : Fin n) => P) (hPpos : ∀ (x : α), 0 < P.real {x}) (hPQ : P.AbsolutelyContinuous Q) (hQpos : ∀ (x : α), 0 < Q.real {x}) {ε δ : ℝ} (hε : 0 < ε) (_hε1 : ε < 1) (hδ : 0 < δ) :

∀ᶠ (n : ℕ) in Filter.atTop , ∃ (s : Set (Fin n → α)), MeasurableSet s ∧ ((MeasureTheory.Measure.pi fun (x : Fin n) => P) sᶜ).toReal ≤ ε ∧ -(1 / ↑n) * Real.log ((MeasureTheory.Measure.pi fun (x : Fin n) => Q) s).toReal ≥ (klDiv P Q).toReal - δ

Stein's lemma (achievability): eventually there exist ε-level tests whose type-II error decays as exp(-n · ((klDiv P Q).toReal − δ)). The statement is in product-measure form; the translation from the random-variable form is supplied by the hypothesis hMapJoint : μ.map (jointRV Xs n) = Measure.pi (fun _ : Fin n => P).

Used by

Tensorization of the KL divergence #

The KL divergence between i.i.d. product measures factorizes as n times the single-sample KL divergence: klDiv (Π_{Fin n} P) (Π_{Fin n} Q) = n · klDiv P Q.

theorem

InformationTheory.Shannon.klDiv_pi_zero

{α : Type u_2} [MeasurableSpace α] (P Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] :

klDiv (MeasureTheory.Measure.pi fun (x : Fin 0) => P) (MeasureTheory.Measure.pi fun (x : Fin 0) => Q) = 0

Base case of the KL tensorization: the product measures over Fin 0 → α agree, so their KL divergence is 0.

Used by

theorem

InformationTheory.Shannon.klDiv_pi_succ

{α : Type u_2} [Fintype α] [MeasurableSpace α] (P Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (n : ℕ) :

klDiv (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => P) (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => Q) = klDiv P Q + klDiv (MeasureTheory.Measure.pi fun (x : Fin n) => P) (MeasureTheory.Measure.pi fun (x : Fin n) => Q)

Step case of the KL tensorization: klDiv (Π_{n+1} P) (Π_{n+1} Q) = klDiv P Q + klDiv (Π_n P) (Π_n Q).

Used by

theorem

InformationTheory.Shannon.klDiv_pi_eq_n_smul

{α : Type u_2} [Fintype α] [MeasurableSpace α] (P Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (n : ℕ) :

klDiv (MeasureTheory.Measure.pi fun (x : Fin n) => P) (MeasureTheory.Measure.pi fun (x : Fin n) => Q) = ↑n * klDiv P Q

KL tensorization: klDiv (Π_{Fin n} P) (Π_{Fin n} Q) = n · klDiv P Q.

Used by