InformationTheory.Shannon.Stein.Converse

Imports 2

Stein's lemma: converse #

The converse (upper bound) side of Stein's lemma. Every ε-level test obeys the matching converse rate bound: the argument reduces the test to a Bernoulli random variable, applies the data-processing inequality together with the KL tensorization, expands the resulting two-point KL divergence into its sum form, and finally sharpens it using the level constraint into the concrete rate bound.

Main statements #

stein_converse_finite_n — every ε-level test obeys the matching converse rate bound -(1/n) log Qⁿ s ≤ (klDiv P Q).toReal / (1−ε) + log 2 / (n(1−ε)).

References #

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

Stein converse #

Every ε-level test obeys the converse rate bound.

theorem

InformationTheory.Shannon.stein_converse_bool_kl_le

source

klDiv (MeasureTheory.Measure.map (InformationTheory.Shannon.steinTestFn✝ n s) (MeasureTheory.Measure.pi fun (x : Fin n) => P)) (MeasureTheory.Measure.map (InformationTheory.Shannon.steinTestFn✝ n s) (MeasureTheory.Measure.pi fun (x : Fin n) => Q)) ≤ ↑n * klDiv P Q

For any test s, the KL divergence between the pushforwards of Pⁿ and Qⁿ along the test indicator is at most n · klDiv P Q.

Used by

theorem

InformationTheory.Shannon.stein_converse_sum_form

source

have Pn := MeasureTheory.Measure.pi fun (x : Fin n) => P; have Qn := MeasureTheory.Measure.pi fun (x : Fin n) => Q; Pn.real s * (Real.log (Pn.real s) - Real.log (Qn.real s)) + Pn.real sᶜ * (Real.log (Pn.real sᶜ) - Real.log (Qn.real sᶜ)) ≤ ↑n * (klDiv P Q).toReal

The two-point sum form of the converse bound: (Pⁿ s)(log Pⁿ s − log Qⁿ s) + (Pⁿ sᶜ)(log Pⁿ sᶜ − log Qⁿ sᶜ) ≤ n · (klDiv P Q).toReal.

Used by

The converse inequality #

The concrete rate bound -(1/n) log Qⁿ s ≤ (klDiv P Q).toReal / (1−ε) + log 2 / (n(1−ε)).

theorem

InformationTheory.Shannon.stein_converse_finite_n

source

{α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] (_hPpos : ∀ (x : α), 0 < P.real {x}) (hPQ : P.AbsolutelyContinuous Q) (hQpos : ∀ (x : α), 0 < Q.real {x}) {ε : ℝ} (_hε : 0 < ε) (hε1 : ε < 1) {n : ℕ} (hn_pos : 0 < n) (s : Set (Fin n → α)) (hs : MeasurableSet s) (hPn_sc_le : ((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 / (1 - ε) + Real.log 2 / (↑n * (1 - ε))

Stein's lemma (converse, finite n): any measurable ε-level test s (with Pⁿ sᶜ ≤ ε) and 0 < n satisfies -(1/n) log Qⁿ s ≤ (klDiv P Q).toReal / (1−ε) + log 2 / (n(1−ε)).

Used by