InformationTheory

InformationTheory.Shannon.Sanov.TendstoSandwich

source

Imports 2

Sanov LDP equality form (Tendsto sandwich) #

Cover-Thomas, simplified open-set form:

(1/n) log Q^n(⋃ c ∈ E n, T_c)  →  -D   as n → ∞

where D = klDivSumForm_ofVec P (Q.real ∘ singleton), given E n eventually contains roundedTypeIndex P n and ∀ c ∈ E n, D ≤ klDivIndex c n Q.

Main statements #

Implementation notes #

References #

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

Tendsto sandwich (main theorem) #

theorem

InformationTheory.Shannon.iUnion_typeClassByCount_pos_of_mem

source
{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] (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) :
0 < ((MeasureTheory.Measure.pi fun (x : Fin n) => Q) (⋃ c ∈ E n, typeClassByCount fun (a : α) => ↑(c a))).toReal
Used by
    theorem

    InformationTheory.Shannon.log_le_inv_mul_log_iUnion_of_forall_le

    source
    {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] (Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure Q] (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) {m : ℝ} (hm_pos : 0 < m) (hm_le : ∀ (a : α), m ≤ Q.real {a}) :
    Real.log m ≤ 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.sanov_ldp_equality

      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) (h_minimizer : ∀ (n : ℕ), ∀ c ∈ E n, (klDivSumForm_ofVec P fun (a : α) => Q.real {a}) ≤ klDivIndex (fun (a : α) => ↑(c a)) n Q) :
      Filter.Tendsto (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 (nhds (-klDivSumForm_ofVec P fun (a : α) => Q.real {a}))

      Sanov's theorem (LDP, equality form):

      (1/n) log Q^n(⋃ c ∈ E n, T_c)  →  -klDivSumForm_ofVec P (Q.real ∘ singleton)

      for the minimizer P whose rounded type sequence eventually lies in E n.

      Used by