InformationTheory.Shannon.Stein.OptimalExponent

Imports 2

Stein's lemma: the optimal type-II exponent #

The achievability and converse bounds are assembled onto the optimal type-II error steinOptimalBeta P Q n ε. The two bounds do not coincide: the converse carries a 1/(1−ε) factor, so the rate -(1/n) log (steinOptimalBeta P Q n ε) is sandwiched between (klDiv P Q).toReal − δ from below and (klDiv P Q).toReal / (1−ε) + log 2 / (n(1−ε)) from above. Letting ε → 0⁺ collapses the upper bound back to (klDiv P Q).toReal.

Main definitions #

steinBetaSet P Q n ε — the type-II error probabilities attainable by ε-level tests.
steinOptimalBeta P Q n ε — the infimum of steinBetaSet, the optimal type-II error.

Main statements #

steinOptimalBeta_log_le_of_converse and steinOptimalBeta_log_ge_of_achievability — the converse and achievability bounds expressed on steinOptimalBeta.

The optimal type-II exponent #

The achievability and converse bounds are lifted onto the optimal type-II error steinOptimalBeta P Q n ε. The two bounds do not coincide: the converse carries a 1/(1−ε) factor, so the rate -(1/n) log (steinOptimalBeta P Q n ε) is sandwiched between (klDiv P Q).toReal − δ from below and (klDiv P Q).toReal / (1−ε) + log 2 / (n(1−ε)) from above. Letting ε → 0⁺ collapses the upper bound back to (klDiv P Q).toReal.

noncomputable def

InformationTheory.Shannon.steinBetaSet

source

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

Set ℝ

The set of type-II error probabilities attainable by ε-level tests.

Equations

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

Instances For

Used by

noncomputable def

InformationTheory.Shannon.steinOptimalBeta

source

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

ℝ

The optimal type-II error subject to type-I ≤ ε.

Equations

InformationTheory.Shannon.steinOptimalBeta P Q n ε = sInf (InformationTheory.Shannon.steinBetaSet P Q n ε)

Instances For

Used by

theorem

InformationTheory.Shannon.one_mem_steinBetaSet

source

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

1 ∈ steinBetaSet P Q n ε

s := Set.univ is always an α-level test (its complement has measure 0).

Used by

theorem

InformationTheory.Shannon.steinBetaSet_nonempty

source

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

(steinBetaSet P Q n ε).Nonempty

Used by

theorem

InformationTheory.Shannon.steinBetaSet_bddBelow

source

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

BddBelow (steinBetaSet P Q n ε)

Used by

theorem

InformationTheory.Shannon.steinOptimalBeta_nonneg

source

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

0 ≤ steinOptimalBeta P Q n ε

Used by

theorem

InformationTheory.Shannon.steinOptimalBeta_le_one

source

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

steinOptimalBeta P Q n ε ≤ 1

Used by

theorem

InformationTheory.Shannon.exp_le_Qn_of_alpha_level

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 : 0 < n) (s : Set (Fin n → α)) (hs : MeasurableSet s) (hα : ((MeasureTheory.Measure.pi fun (x : Fin n) => P) sᶜ).toReal ≤ ε) :

Real.exp (-(↑n * ((klDiv P Q).toReal / (1 - ε) + Real.log 2 / (↑n * (1 - ε))))) ≤ ((MeasureTheory.Measure.pi fun (x : Fin n) => Q) s).toReal

Exponential form of the converse: for any ε-level test s, exp(-n · ((klDiv P Q).toReal / (1−ε) + log 2 / (n(1−ε)))) ≤ Qⁿ s.

Used by

theorem

InformationTheory.Shannon.exp_le_steinOptimalBeta

source

Real.exp (-(↑n * ((klDiv P Q).toReal / (1 - ε) + Real.log 2 / (↑n * (1 - ε))))) ≤ steinOptimalBeta P Q n ε

The optimal type-II error is bounded below in exponential form: exp(-n · ((klDiv P Q).toReal / (1−ε) + log 2 / (n(1−ε)))) ≤ steinOptimalBeta P Q n ε.

Used by

theorem

InformationTheory.Shannon.steinOptimalBeta_pos

source

0 < steinOptimalBeta P Q n ε

The optimal type-II error steinOptimalBeta is strictly positive.

Used by

theorem

InformationTheory.Shannon.steinOptimalBeta_log_le_of_converse

source

-(1 / ↑n) * Real.log (steinOptimalBeta P Q n ε) ≤ (klDiv P Q).toReal / (1 - ε) + Real.log 2 / (↑n * (1 - ε))

Converse-side upper bound on the type-II exponent: -(1/n) log (steinOptimalBeta P Q n ε) ≤ (klDiv P Q).toReal / (1−ε) + log 2 / (n(1−ε)).

Used by

theorem

InformationTheory.Shannon.steinOptimalBeta_log_ge_of_achievability

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 < δ) :

∀ᶠ (n : ℕ) in Filter.atTop , (klDiv P Q).toReal - δ ≤ -(1 / ↑n) * Real.log (steinOptimalBeta P Q n ε)

Achievability-side lower bound on the type-II exponent: eventually (klDiv P Q).toReal − δ ≤ -(1/n) log (steinOptimalBeta P Q n ε).

Used by