InformationTheory.Shannon.Hoeffding.Tradeoff

Imports 9

Hoeffding tradeoff exponent — scaffolding and variational form #

Scaffolding towards Cover-Thomas.x:

-(1/n) log β_n(alpha) → hoeffdingE2 P₁ P₂ alpha

hoeffdingE2, hoeffdingE2_attained, and hoeffdingE2_unique are published in InformationTheory/Shannon/Chernoff/Basic.lean. This file adds the pmf-form infrastructure and the Pythagoras-based minimizer bound.

Main definitions #

pmfToMeasure — lift a pmf vector to Measure α via PMF.ofFintype.
steinBetaSet_pmf — set of achievable Type II errors at Type I level alpha (pmf form).
steinTypeII_at_level_pmf — optimal Type II error (pmf form).

Main statements #

hoeffdingConstraintSet_convex — the Hoeffding constraint set is convex.
hoeffding_minimizer_ge — Csiszar Pythagoras gives klDivPmf Qstar P₂ ≤ klDivPmf P P₂ for any P ∈ K with full support, when Qstar is the minimizer.

Implementation notes #

This file provides the variational scaffolding; the full sandwich Tendsto (achievability from Sanov LDP + converse from Stein typicality) is in Hoeffding/TradeoffExp.lean.
The pmf ↔ Measure bridge uses PMF.ofFintype + PMF.toMeasure (~4 lemmas).

pmf ↔ Measure bridge (helper) #

noncomputable def

InformationTheory.Shannon.HoeffdingTradeoff.pmfToMeasure

source

{α : Type u_1} [Fintype α] [MeasurableSpace α] (P : α → ℝ) (hP_nn : ∀ (a : α), 0 ≤ P a) (hP_sum : ∑ a : α, P a = 1) :

MeasureTheory.Measure α

Lift a pmf vector P : α → ℝ to Measure α via PMF.ofFintype.

Equations

InformationTheory.Shannon.HoeffdingTradeoff.pmfToMeasure P hP_nn hP_sum = (PMF.ofFintype (fun (a : α) => ENNReal.ofReal (P a)) ⋯).toMeasure

Instances For

Used by

instance

InformationTheory.Shannon.HoeffdingTradeoff.pmfToMeasure_isProbabilityMeasure

source

{α : Type u_1} [Fintype α] [MeasurableSpace α] (P : α → ℝ) (hP_nn : ∀ (a : α), 0 ≤ P a) (hP_sum : ∑ a : α, P a = 1) :

MeasureTheory.IsProbabilityMeasure (pmfToMeasure P hP_nn hP_sum)

Used by

theorem

InformationTheory.Shannon.HoeffdingTradeoff.pmfToMeasure_apply_singleton

source

{α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P : α → ℝ) (hP_nn : ∀ (a : α), 0 ≤ P a) (hP_sum : ∑ a : α, P a = 1) (a : α) :

(pmfToMeasure P hP_nn hP_sum) {a} = ENNReal.ofReal (P a)

Used by

theorem

InformationTheory.Shannon.HoeffdingTradeoff.pmfToMeasure_real_singleton

source

{α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P : α → ℝ) (hP_nn : ∀ (a : α), 0 ≤ P a) (hP_sum : ∑ a : α, P a = 1) (a : α) :

(pmfToMeasure P hP_nn hP_sum).real {a} = P a

Used by

`steinTypeII_at_level_pmf` definition and basic properties #

noncomputable def

InformationTheory.Shannon.HoeffdingTradeoff.steinBetaSet_pmf

source

{α : Type u_1} (P₁ P₂ : α → ℝ) (n : ℕ) (alpha : ℝ) :

Set ℝ

n-IID Type II error set (pmf form).

s : Finset (Fin n → α) is the acceptance region for H₀. The Type I error is 1 - ∑_{x ∈ s} ∏ P₁(x_i) and the Type II error is ∑_{x ∈ s} ∏ P₂(x_i). Convention matches Stein/OptimalExponent.lean :: steinBetaSet (Measure path) with Finset instead of Set + MeasurableSet.

Equations

InformationTheory.Shannon.HoeffdingTradeoff.steinBetaSet_pmf P₁ P₂ n alpha = {β : ℝ | ∃ (s : Finset (Fin n → α)), 1 - ∑ x ∈ s, ∏ i : Fin n, P₁ (x i) ≤ alpha ∧ β = ∑ x ∈ s, ∏ i : Fin n, P₂ (x i)}

Instances For

Used by

noncomputable def

InformationTheory.Shannon.HoeffdingTradeoff.steinTypeII_at_level_pmf

source

{α : Type u_1} (P₁ P₂ : α → ℝ) (n : ℕ) (alpha : ℝ) :

ℝ

Optimal Type II error (pmf form).

Equations

InformationTheory.Shannon.HoeffdingTradeoff.steinTypeII_at_level_pmf P₁ P₂ n alpha = sInf (InformationTheory.Shannon.HoeffdingTradeoff.steinBetaSet_pmf P₁ P₂ n alpha)

Instances For

Used by

theorem

InformationTheory.Shannon.HoeffdingTradeoff.sum_prod_pi_eq_pow_sum

source

{α : Type u_1} [Fintype α] (P : α → ℝ) (n : ℕ) :

∑ x : Fin n → α, ∏ i : Fin n, P (x i) = (∑ a : α, P a) ^ n

∑_{x : Fin n → α} ∏ i, P (x i) = (∑ a, P a)^n for pmf-like vectors.

Used by

theorem

InformationTheory.Shannon.HoeffdingTradeoff.one_mem_steinBetaSet_pmf

source

{α : Type u_1} [Fintype α] (P₁ P₂ : α → ℝ) (hP₁_sum : ∑ a : α, P₁ a = 1) (hP₂_sum : ∑ a : α, P₂ a = 1) (n : ℕ) (alpha : ℝ) (h_alpha_nn : 0 ≤ alpha) :

1 ∈ steinBetaSet_pmf P₁ P₂ n alpha

1 ∈ steinBetaSet_pmf (take s := univ).

Used by

theorem

InformationTheory.Shannon.HoeffdingTradeoff.steinTypeII_at_level_pmf_nonneg

source

{α : Type u_1} [Fintype α] (P₁ P₂ : α → ℝ) (hP₁_sum : ∑ a : α, P₁ a = 1) (hP₂_sum : ∑ a : α, P₂ a = 1) (hP₂_nn : ∀ (a : α), 0 ≤ P₂ a) (n : ℕ) (alpha : ℝ) (h_alpha_nn : 0 ≤ alpha) :

0 ≤ steinTypeII_at_level_pmf P₁ P₂ n alpha

steinTypeII_at_level_pmf P₁ P₂ n alpha ≥ 0.

Used by

theorem

InformationTheory.Shannon.HoeffdingTradeoff.steinTypeII_at_level_pmf_le_one

source

steinTypeII_at_level_pmf P₁ P₂ n alpha ≤ 1

steinTypeII_at_level_pmf P₁ P₂ n alpha ≤ 1.

Used by

Hoeffding constraint set convexity + Qstar full support #

theorem

InformationTheory.Shannon.HoeffdingTradeoff.hoeffdingConstraintSet_convex

source

{α : Type u_1} [Fintype α] (P₁ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (alpha : ℝ) :

Convex ℝ (Chernoff.hoeffdingConstraintSet P₁ alpha)

The Hoeffding constraint set is convex: intersection of the convex simplex with the convex sublevel set of the convex functional Q ↦ klDivPmf Q P₁.

Used by

Pythagoras-based minimizer bound #

theorem

InformationTheory.Shannon.HoeffdingTradeoff.hoeffding_minimizer_ge

source

{α : Type u_1} [Fintype α] [Nonempty α] (P₁ P₂ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (_hP₁_sum : ∑ a : α, P₁ a = 1) (hP₂_sum : ∑ a : α, P₂ a = 1) (alpha : ℝ) (_h_alpha_nn : 0 ≤ alpha) {Qstar : α → ℝ} (hQs_mem : Qstar ∈ Chernoff.hoeffdingConstraintSet P₁ alpha) (hQs_pos : ∀ (a : α), 0 < Qstar a) (hQs_min : Chernoff.hoeffdingE2 P₁ P₂ alpha = CsiszarProjection.klDivPmf Qstar P₂) {P : α → ℝ} (hP_mem : P ∈ Chernoff.hoeffdingConstraintSet P₁ alpha) (hP_pos : ∀ (a : α), 0 < P a) :

CsiszarProjection.klDivPmf Qstar P₂ ≤ CsiszarProjection.klDivPmf P P₂

Hoeffding Sanov minimizer: for any P ∈ K with full support and minimizer Qstar, klDivPmf Qstar P₂ ≤ klDivPmf P P₂.

Used by

InformationTheory.Shannon.Hoeffding.Tradeoff

Hoeffding tradeoff exponent — scaffolding and variational form #

Main definitions #

Main statements #

Implementation notes #

pmf ↔ Measure bridge (helper) #

steinTypeII_at_level_pmf definition and basic properties #

Hoeffding constraint set convexity + Qstar full support #

Pythagoras-based minimizer bound #

`steinTypeII_at_level_pmf` definition and basic properties #