InformationTheory.Shannon.StrongTypicality
Strong typicality (Cover-Thomas) #
Three main theorems for the strongly typical set
A^*_ε^n := { x : Fin n → α | ∀ a, |(typeCount x a : ℝ)/n - P(a)| ≤ ε }:
stronglyTypicalSet_prob_tendsto_one—μ {ω | jointRV ∈ A^*} → 1(WLLN on indicators).- (size upper bound) —
|A^*| ≤ exp(n(H + ε·L))via the strong-to-weak inclusion. stronglyTypicalSet_card_ge_eventually—∃ N, ∀ n ≥ N, (1-η)·exp(n(H - ε·L - δ)) ≤ |A^*|.
Here L := logSumAbs μ Xs = ∑ a, |log P(a)|, N(a|x^n) := typeCount x a,
P(a) := (μ.map (Xs 0)).real {a}, H := entropy μ (Xs 0).
Main definitions #
stronglyTypicalSet— the strongly typical setA^*_ε^n.logSumAbs— the Lipschitz constant∑ a, |log P(a)|of the strong-to-weak bridge.
Main statements #
stronglyTypicalSet_prob_tendsto_one— probability of the typical set tends to 1.stronglyTypicalSet_card_ge_eventually— lower size bound (eventually inn).
Implementation notes #
The WLLN is applied per letter via strong_law_ae_real on the indicators
Y_a i ω := 𝟙(Xs i ω = a), then a union bound over the finite alphabet α
gives simultaneous concentration. Full support hpos : ∀ a, 0 < P(a) is
required for the size bounds (via typicalSet_prob_le) but not for the
probability convergence.
References #
- T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.
Definitions #
InformationTheory.Shannon.stronglyTypicalSet
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[DecidableEq α]
[MeasurableSpace α]
(μ : MeasureTheory.Measure Ω)
(Xs : ℕ → Ω → α)
(n : ℕ)
(ε : ℝ)
:
The strongly typical set
A^*_ε^n := { x : Fin n → α | ∀ a, |(typeCount x a : ℝ)/n - P(a)| ≤ ε }.
Equations
Instances For
Used by
InformationTheory.Shannon.mem_stronglyTypicalSet_iff
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
(Xs : ℕ → Ω → α)
(n : ℕ)
(ε : ℝ)
(x : Fin n → α)
:
Used by
InformationTheory.Shannon.measurableSet_stronglyTypicalSet
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
(Xs : ℕ → Ω → α)
(n : ℕ)
(ε : ℝ)
:
MeasurableSet (stronglyTypicalSet μ Xs n ε)
Used by
Probability convergence #
InformationTheory.Shannon.letterIndicator
sourceInstances For
Used by
InformationTheory.Shannon.measurable_letterIndicator
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(Xs : ℕ → Ω → α)
(hXs : ∀ (i : ℕ), Measurable (Xs i))
(a : α)
(i : ℕ)
:
Measurable (letterIndicator Xs a i)
Used by
InformationTheory.Shannon.indepFun_letterIndicator
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
(Xs : ℕ → Ω → α)
(_hXs : ∀ (i : ℕ), Measurable (Xs i))
(hindep : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ)
(a : α)
:
Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (letterIndicator Xs a i) (letterIndicator Xs a j) μ
Used by
InformationTheory.Shannon.identDistrib_letterIndicator
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
(Xs : ℕ → Ω → α)
(hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ)
(a : α)
(i : ℕ)
:
ProbabilityTheory.IdentDistrib (letterIndicator Xs a i) (letterIndicator Xs a 0) μ μ
Used by
InformationTheory.Shannon.integral_letterIndicator
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : ℕ → Ω → α)
(hXs : ∀ (i : ℕ), Measurable (Xs i))
(a : α)
:
Used by
InformationTheory.Shannon.integrable_letterIndicator
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : ℕ → Ω → α)
(hXs : ∀ (i : ℕ), Measurable (Xs i))
(a : α)
:
MeasureTheory.Integrable (letterIndicator Xs a 0) μ
Used by
InformationTheory.Shannon.typeCount_eq_sum_indicator
source{α : Type u_2}
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
{n : ℕ}
(x : Fin n → α)
(a : α)
:
Used by
InformationTheory.Shannon.letterIndicator_inProbability
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(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) μ μ)
(a : α)
{ε : ℝ}
(hε : 0 < ε)
:
Filter.Tendsto
(fun (n : ℕ) =>
μ
{ω : Ω | ε ≤ |(∑ i ∈ Finset.range n, letterIndicator Xs a i ω) / ↑n - (MeasureTheory.Measure.map (Xs 0) μ).real {a}|})
Filter.atTop (nhds 0)
Used by
InformationTheory.Shannon.stronglyTypicalSet_prob_tendsto_one
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(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) μ μ)
{ε : ℝ}
(hε : 0 < ε)
:
Filter.Tendsto (fun (n : ℕ) => μ {ω : Ω | jointRV Xs n ω ∈ stronglyTypicalSet μ Xs n ε}) Filter.atTop (nhds 1)
For Xs i.i.d. with a finite alphabet, the probability of the strongly typical set tends
to one, μ {ω | jointRV Xs n ω ∈ A^*_ε^n} → 1.
Used by
Strong-to-weak typicality bridge #
InformationTheory.Shannon.logSumAbs
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[MeasurableSpace α]
(μ : MeasureTheory.Measure Ω)
(Xs : ℕ → Ω → α)
:
Lipschitz constant ∑ a, |log P(a)| of the strong-to-weak typicality bridge.
Equations
- InformationTheory.Shannon.logSumAbs μ Xs = ∑ a : α, |Real.log ((MeasureTheory.Measure.map (Xs 0) μ).real {a})|
Instances For
Used by
InformationTheory.Shannon.logSumAbs_nonneg
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
(Xs : ℕ → Ω → α)
:
Used by
InformationTheory.Shannon.weak_displacement_eq_strong_sum
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : ℕ → Ω → α)
(_hXs : ∀ (i : ℕ), Measurable (Xs i))
{n : ℕ}
(hn : 0 < n)
(x : Fin n → α)
:
Used by
InformationTheory.Shannon.stronglyTypical_implies_weakly_typical_bound
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : ℕ → Ω → α)
(hXs : ∀ (i : ℕ), Measurable (Xs i))
{n : ℕ}
(hn : 0 < n)
{ε : ℝ}
(x : Fin n → α)
(hx : x ∈ stronglyTypicalSet μ Xs n ε)
:
Used by
InformationTheory.Shannon.stronglyTypicalSet_subset_typicalSet
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : ℕ → Ω → α)
(hXs : ∀ (i : ℕ), Measurable (Xs i))
{n : ℕ}
(hn : 0 < n)
{ε ε' : ℝ}
(h_bound : ε * logSumAbs μ Xs < ε')
:
Used by
Size bounds #
InformationTheory.Shannon.stronglyTypicalSet_card_ge_eventually
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : ℕ → Ω → α)
(hXs : ∀ (i : ℕ), Measurable (Xs i))
(hindep_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ)
(hindep_pair : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ)
(hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ)
(hpos : ∀ (a : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {a})
{ε δ η : ℝ}
(hε : 0 < ε)
(hδ : 0 < δ)
(hη : 0 < η)
:
A lower bound on the typical-set size (eventually-N form): for any η > 0,
eventually |A^*_ε^n| ≥ (1-η) · exp(n · (H - ε·L - δ)).