InformationTheory.Shannon.Sanov.LDP

Imports 5

Sanov's theorem — LDP upper bound (B form) #

Cover-Thomas: for any family E n ⊆ TypeCountIndex α n,

(1/n) log Q^n({x | typeCount x ∈ E n}) ≤ -D* + ε   (eventually)

where D* = inf_{c ∈ E n} klDivIndex c n Q.

Main definitions #

TypeCountIndex α n — abbreviation for α → Fin (n+1), the type used to index empirical count vectors.
typeClassByCount c — the type class {x | ∀ a, typeCount x a = c a}.
klDivIndex c n Q — KL divergence of the rational distribution c/n from Q, defined as ∑ a, (c a / n) * (log (c a / n) - log Q.real {a}).

Main statements #

typeCountIndex_card — |TypeCountIndex α n| = (n+1)^|α| (polynomial cardinality bound).
typeClassByCount_Qn_le — Q^n(typeClassByCount c) ≤ exp(-n · klDivIndex c n Q).
typeClassByCount_union_Qn_le_inf — union-form bound: Q^n(⋃ c ∈ F, T_c) ≤ |F| · exp(-n · D*).
sanov_ldp_upper_bound — LDP upper bound with o(1) slack via |α| log(n+1)/n → 0.

Implementation notes #

The bound on typeClassByCount c is proved self-containedly (index form) rather than by reducing to the A-form typeClass_Qn_le, because the rational distribution c/n may have zero components when c a = 0, violating the full-support hypothesis.
The polynomial slack (|α| log(n+1))/n → 0 is extracted from Real.isLittleO_log_id_atTop.

References #

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

Type-count index + polynomial bound #

abbrev

InformationTheory.Shannon.TypeCountIndex

source

@[reducible, inline]

(α : Type u_2) [Fintype α] (n : ℕ) :

Type u_2

Type-count index: α → Fin (n+1), indexing empirical count vectors. Inconsistent indices (∑ ≠ n) yield an empty type class.

Equations

InformationTheory.Shannon.TypeCountIndex α n = (α → Fin (n + 1))

Instances For

Used by

instance

InformationTheory.Shannon.instFintypeTypeCountIndex

source

@[implicit_reducible]

{α : Type u_1} [DecidableEq α] [Fintype α] (n : ℕ) :

Fintype (TypeCountIndex α n)

Equations

InformationTheory.Shannon.instFintypeTypeCountIndex n = id inferInstance

Used by

theorem

InformationTheory.Shannon.typeCountIndex_card

source

{α : Type u_1} [Fintype α] [DecidableEq α] (n : ℕ) :

Fintype.card (TypeCountIndex α n) = (n + 1) ^ Fintype.card α

Polynomial cardinality bound: |TypeCountIndex α n| = (n+1)^|α|.

Used by

Type class by integer counts + Sanov bound #

def

InformationTheory.Shannon.typeClassByCount

source

{α : Type u_1} [DecidableEq α] {n : ℕ} (c : α → ℕ) :

Set (Fin n → α)

Type class by integer counts T(c) := {x | ∀ a, typeCount x a = c a}.

Equations

InformationTheory.Shannon.typeClassByCount c = {x : Fin n → α | ∀ (a : α), InformationTheory.Shannon.typeCount x a = c a}

Instances For

Used by

noncomputable def

InformationTheory.Shannon.klDivIndex

source

{α : Type u_1} [Fintype α] [MeasurableSpace α] (c : α → ℕ) (n : ℕ) (Q : MeasureTheory.Measure α) :

ℝ

KL divergence at an empirical type (rational form): klDivIndex c n Q := ∑ a, (c a / n) · (log (c a / n) - log Q.real{a}).

Equations

InformationTheory.Shannon.klDivIndex c n Q = ∑ a : α, ↑(c a) / ↑n * (Real.log (↑(c a) / ↑n) - Real.log (Q.real {a}))

Instances For

Used by

theorem

InformationTheory.Shannon.sum_const_aggr_of_mem_typeClassByCount

source

{α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} {c : α → ℕ} {x : Fin n → α} (hx : x ∈ typeClassByCount c) (f : α → ℝ) :

∑ i : Fin n, f (x i) = ∑ a : α, ↑(c a) * f a

Used by

theorem

InformationTheory.Shannon.typeClassByCount_prod_eq

source

{α : Type u_1} [Fintype α] [DecidableEq α] [MeasurableSpace α] (Q : MeasureTheory.Measure α) (hQpos : ∀ (a : α), 0 < Q.real {a}) {n : ℕ} (hn : 0 < n) {c : α → ℕ} {x : Fin n → α} (hx : x ∈ typeClassByCount c) :

∏ i : Fin n, Q.real {x i} = (∏ a : α, (↑(c a) / ↑n) ^ c a) * Real.exp (-(↑n * klDivIndex c n Q))

Per-point identity (index form): x ∈ typeClassByCount c implies ∏ i, Q.real {x i} = (∏ a, ((c a : ℝ)/n)^(c a)) · exp(-n · klDivIndex c n Q).

Used by

theorem

InformationTheory.Shannon.typeClassByCount_Qn_le

source

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure Q] (hQpos : ∀ (a : α), 0 < Q.real {a}) {n : ℕ} (hn : 0 < n) (c : α → ℕ) (hc_sum : ∑ a : α, c a = n) :

((MeasureTheory.Measure.pi fun (x : Fin n) => Q) (typeClassByCount c)).toReal ≤ Real.exp (-(↑n * klDivIndex c n Q))

Sanov upper bound (index form): for c : α → ℕ with ∑ c a = n, Q^n(typeClassByCount c) ≤ exp(-n · klDivIndex c n Q).

Used by

Union form upper bound + LDP main statement #

theorem

InformationTheory.Shannon.typeClassByCount_empty_of_sum_ne

source

{α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} {c : α → ℕ} (h : ∑ a : α, c a ≠ n) :

typeClassByCount c = ∅

If ∑ c a ≠ n then typeClassByCount c = ∅.

Used by

theorem

InformationTheory.Shannon.typeClassByCount_union_Qn_le

source

((MeasureTheory.Measure.pi fun (x : Fin n) => Q) (⋃ c ∈ F, typeClassByCount fun (a : α) => ↑(c a))).toReal ≤ ∑ c ∈ F, Real.exp (-(↑n * klDivIndex (fun (a : α) => ↑(c a)) n Q))

Union form upper bound: for any F : Finset (TypeCountIndex α n), Q^n(⋃ c ∈ F, typeClassByCount c) ≤ ∑ c ∈ F, exp(-n · klDivIndex c n Q).

Used by

theorem

InformationTheory.Shannon.typeClassByCount_union_Qn_le_inf

source

((MeasureTheory.Measure.pi fun (x : Fin n) => Q) (⋃ c ∈ F, typeClassByCount fun (a : α) => ↑(c a))).toReal ≤ ↑F.card * Real.exp (-(↑n * D))

inf-form upper bound: if ∀ c ∈ F, D ≤ klDivIndex c n Q then Q^n(⋃ c ∈ F, typeClassByCount c) ≤ |F| · exp(-n · D).

Used by

theorem

InformationTheory.Shannon.log_succ_div_tendsto_zero

source

Filter.Tendsto (fun (n : ℕ) => Real.log (↑n + 1) / ↑n) Filter.atTop (nhds 0)

Real.log (n+1) / n → 0 as n → ∞.

Used by

theorem

InformationTheory.Shannon.sanov_ldp_upper_bound

source

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure Q] (hQpos : ∀ (a : α), 0 < Q.real {a}) (E : (n : ℕ) → Finset (TypeCountIndex α n)) (D : ℝ) (hD : ∀ (n : ℕ), ∀ c ∈ E n, D ≤ klDivIndex (fun (a : α) => ↑(c a)) n Q) {ε : ℝ} (hε : 0 < ε) :

∃ (N : ℕ), ∀ n ≥ N, 0 < n → 0 < ((MeasureTheory.Measure.pi fun (x : Fin n) => Q) (⋃ c ∈ E n, typeClassByCount fun (a : α) => ↑(c a))).toReal → 1 / ↑n * Real.log ((MeasureTheory.Measure.pi fun (x : Fin n) => Q) (⋃ c ∈ E n, typeClassByCount fun (a : α) => ↑(c a))).toReal ≤ -D + ε

Sanov's theorem (LDP upper bound): (1/n) log Q^n({x | typeCount x ∈ E n}) ≤ -D + ε for all large n, provided every c ∈ E n satisfies D ≤ klDivIndex c n Q.

Used by