InformationTheory.Shannon.Sanov.LiminfBound

Imports 2

Sanov LDP liminf lower bound #

The liminf lower bound for Sanov's theorem (Cover-Thomas): liminf (1/n) log Q^n(⋃ c ∈ E n, T_c) ≥ -D, extracted by sandwiching the per-n lower bound with |α| log(n+1)/n → 0.

Main statements #

sanov_ldp_lower_bound_pointwise — liminf (1/n) log Q^n(⋃ c ∈ E n, T_c) ≥ -D.

Implementation notes #

The liminf bound is extracted by sandwiching with |α| log(n+1)/n → 0.

References #

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

liminf lower bound #

theorem

InformationTheory.Shannon.neg_card_mul_logSucc_div_sub_klDivIndex_le_inv_mul_log_iUnion

source

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure Q] (hQpos : ∀ (a : α), 0 < Q.real {a}) (P : α → ℝ) (hP_prob : ∑ a : α, P a = 1) (hP_nn : ∀ (a : α), 0 ≤ P a) (E : (n : ℕ) → Finset (TypeCountIndex α n)) {n : ℕ} (hn_pos : 0 < n) (h_inE : roundedTypeIndex P n ∈ E n) :

-↑(Fintype.card α) * (Real.log (↑n + 1) / ↑n) - klDivIndex (fun (a : α) => ↑(roundedTypeIndex P n a)) n Q ≤ 1 / ↑n * Real.log ((MeasureTheory.Measure.pi fun (x : Fin n) => Q) (⋃ c ∈ E n, typeClassByCount fun (a : α) => ↑(c a))).toReal

Used by

theorem

InformationTheory.Shannon.inv_mul_log_iUnion_typeClassByCount_le_zero

source

{α : Type u_1} [Fintype α] [DecidableEq α] [MeasurableSpace α] (Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure Q] (E : (n : ℕ) → Finset (TypeCountIndex α n)) {n : ℕ} (hn_pos : 0 < n) :

1 / ↑n * Real.log ((MeasureTheory.Measure.pi fun (x : Fin n) => Q) (⋃ c ∈ E n, typeClassByCount fun (a : α) => ↑(c a))).toReal ≤ 0

Used by

theorem

InformationTheory.Shannon.sanov_ldp_lower_bound_pointwise

source

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure Q] (hQpos : ∀ (a : α), 0 < Q.real {a}) (P : α → ℝ) (hP_prob : ∑ a : α, P a = 1) (hP_full : ∀ (a : α), 0 < P a) (E : (n : ℕ) → Finset (TypeCountIndex α n)) (h_in_E : ∀ᶠ (n : ℕ) in Filter.atTop , roundedTypeIndex P n ∈ E n) :

(-klDivSumForm_ofVec P fun (a : α) => Q.real {a}) ≤ Filter.liminf (fun (n : ℕ) => 1 / ↑n * Real.log ((MeasureTheory.Measure.pi fun (x : Fin n) => Q) (⋃ c ∈ E n, typeClassByCount fun (a : α) => ↑(c a))).toReal) Filter.atTop

Sanov's theorem (LDP lower bound): if roundedTypeIndex P n ∈ E n eventually, then liminf (1/n) log Q^n(⋃ c ∈ E n, T_c) ≥ -klDivSumForm_ofVec P (Q.real ∘ singleton).

Used by