InformationTheory.Shannon.StrongStein
Strong Stein's lemma — convergence to KL divergence #
The strong converse for binary hypothesis testing (Cover–Thomas):
for any ε ∈ (0, 1),
-(1/n) * log (steinOptimalBeta P Q n ε) converges to (klDiv P Q).toReal as n → ∞.
Main statements #
steinOptimalBeta_log_le_of_strong_converse— the limsup bound,-(1/n) log β*(n, ε) ≤ K + δ + o(1)(eventually for eachδ > 0).
Implementation notes #
The proof uses an LLR-typicality route (no Pinsker/Sanov). The key step is a
lower bound Q^n(s) ≥ exp(-n(K+δ)) · (P^n(T_n^δ) - ε) for any α-level test s,
derived by restricting to the Stein-typical set. Together with the existing achievability
upper bound, this sandwiches the limit. The existing Stein/ API is reused without
modification.
References #
- T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.
Q^n lower bound on the Stein-typical set #
Strong-converse lower bound for any α-level test #
InformationTheory.Shannon.StrongStein.steinTypicalSubset_Q_prob_ge
source{α : 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 : ℕ}
{δ : ℝ}
(A : Set (Fin n → α))
(hAsub : A ⊆ steinTypicalSet P Q n δ)
:
Used by
InformationTheory.Shannon.StrongStein.steinAlphaTest_Q_prob_ge
source{α : 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 : ℕ}
(s : Set (Fin n → α))
(hs : MeasurableSet s)
(hα : ((MeasureTheory.Measure.pi fun (x : Fin n) => P) sᶜ).toReal ≤ ε)
:
For any measurable s with P^n(sᶜ).toReal ≤ ε,
Q^n(s) ≥ exp(-n(K+δ)) · (P^n(T_n^δ) - ε).
Used by
Main theorem: Tendsto → K #
InformationTheory.Shannon.StrongStein.exp_le_steinOptimalBeta_strong
source{α : 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})
{ε δ : ℝ}
(hε : 0 ≤ ε)
(n : ℕ)
:
Real.exp (-(↑n * ((klDiv P Q).toReal + δ))) * (((MeasureTheory.Measure.pi fun (x : Fin n) => P) (steinTypicalSet P Q n δ)).toReal - ε) ≤ steinOptimalBeta P Q n ε
Used by
InformationTheory.Shannon.StrongStein.steinOptimalBeta_log_le_of_strong_converse
source{Ω : 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 < δ)
:
Strong Stein's lemma: for any δ > 0, eventually
-(1/n) log β*(n, ε) ≤ (klDiv P Q).toReal + δ + o(1).