Skip to content

InformationTheory.Shannon.AEP.Rate

Imports 5

AEP — rate-uniform form (via Chebyshev) #

typicalSet_prob_tendsto_one gives only the Tendsto … (𝓝 1) form and carries no closed-form bound. This module establishes an explicit N(ε, η) with

n ≥ N → μ {ω | jointRV Xs n ω ∈ typicalSet μ Xs n ε} ≥ 1 - η

via the Chebyshev inequality (ProbabilityTheory.meas_ge_le_variance_div_sq) and the pairwise variance sum (ProbabilityTheory.IndepFun.variance_sum).

Since pmfLog μ Xs : α → ℝ is a finite function on the alphabet, each logLikelihood μ Xs i is a.s. bounded by the range of pmfLog (a finite set), hence MemLp _ 2 μ, which supplies the integrability ingredients.

noncomputable def

InformationTheory.Shannon.pmfLogBound

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) :

The supremum of |pmfLog μ Xs| over the alphabet.

Equations

InformationTheory.Shannon.pmfLogBound μ Xs = Finset.univ.sup' ⋯ fun (a : α) => |InformationTheory.Shannon.pmfLog μ Xs a|

Instances For

Used by

theorem

InformationTheory.Shannon.abs_pmfLog_le_bound

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (a : α) :

|pmfLog μ Xs a| ≤ pmfLogBound μ Xs

Used by

theorem

InformationTheory.Shannon.abs_logLikelihood_le_bound

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (i : ℕ) (ω : Ω) :

|logLikelihood μ Xs i ω| ≤ pmfLogBound μ Xs

Used by

theorem

InformationTheory.Shannon.memLp_logLikelihood

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (i : ℕ) :

MeasureTheory.MemLp (logLikelihood μ Xs i) 2 μ

Used by

noncomputable def

InformationTheory.Shannon.pmfLogVariance

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) :

The single-symbol variance Var[logLikelihood μ Xs 0; μ]. The 0-th index suffices because all Xs i are identically distributed.

Equations

InformationTheory.Shannon.pmfLogVariance μ Xs = ProbabilityTheory.variance (InformationTheory.Shannon.logLikelihood μ Xs 0) μ

Instances For

Used by

theorem

InformationTheory.Shannon.pmfLogVariance_nonneg

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) :

0 ≤ pmfLogVariance μ Xs

Used by

theorem

InformationTheory.Shannon.pmfLogVariance_le_sq_of_bounded

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) {B : ℝ} (hB : ∀ (a : α), |pmfLog μ Xs a| ≤ B) :

pmfLogVariance μ Xs ≤ B ^ 2

A pointwise bound |pmfLog Xs a| ≤ B gives pmfLogVariance ≤ B².

Used by

theorem

InformationTheory.Shannon.variance_logLikelihood_eq

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (i : ℕ) :

ProbabilityTheory.variance (logLikelihood μ Xs i) μ = pmfLogVariance μ Xs

Used by

theorem

InformationTheory.Shannon.aep_chebyshev_bound

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [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 < ε) {n : ℕ} (hn : 0 < n) :

μ {ω : Ω | ε ≤ |(∑ i ∈ Finset.range n, logLikelihood μ Xs i ω) / ↑n - entropy μ (Xs 0)|} ≤ ENNReal.ofReal (pmfLogVariance μ Xs / (↑n * ε ^ 2))

Explicit-rate version of aep_inProbability: for n ≥ 1 and ε > 0, μ {ω | ε ≤ |(∑ i ∈ range n, logLikelihood μ Xs i ω) / n - H|} ≤ ENNReal.ofReal (pmfLogVariance μ Xs / (n * ε^2)).

Used by

theorem

InformationTheory.Shannon.typicalSet_prob_ge_of_rate

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [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 < ε) {η : ℝ} (hη : 0 < η) :

∃ (N : ℕ), ∀ n ≥ N, 1 - η ≤ (μ {ω : Ω | jointRV Xs n ω ∈ typicalSet μ Xs n ε}).toReal

Asymptotic equipartition property (explicit rate): for any ε, η > 0, there is N(ε, η) such that for all n ≥ N, the typical set has μ-measure ≥ 1 - η. The explicit bound is N := ⌈pmfLogVariance / (η · ε²)⌉ + 1, so n ≥ N ⇒ pmfLogVariance / (n · ε²) ≤ η.

Used by

theorem

InformationTheory.Shannon.exp_neg_mul_lt_of_rate

{g ε' : ℝ} (hg : 0 < g) (hε' : 0 < ε') :

∃ (N : ℕ), ∀ n ≥ N, Real.exp (-↑n * g) < ε'

Closed-form N(g, ε') for exponential decay: for any g, ε' > 0, there is N such that exp(- n · g) < ε' for all n ≥ N. Concretely N := ⌈max 0 (-log ε' / g)⌉ + 1.

Used by

theorem

InformationTheory.Shannon.channelCoding_E2_lt_of_rate

{I R ε ε' : ℝ} (hgap : 0 < I - R - 3 * ε) (hε' : 0 < ε') :

∃ (N : ℕ), ∀ n ≥ N, (↑⌈Real.exp (↑n * R)⌉₊ - 1) * Real.exp (↑n * (-I + 3 * ε)) < ε'

Closed-form N(I, R, ε, ε') for the channel-coding E2 term. Given the AEP gap g := I - R - 3ε > 0 and any tolerance ε' > 0, there is N such that (⌈exp(n·R)⌉ - 1) · exp(n · (-I + 3ε)) < ε' for all n ≥ N.

Used by

theorem

InformationTheory.Shannon.jointlyTypicalSet_prob_ge_of_rate

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {β : Type u_3} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hYs : ∀ (i : ℕ), Measurable (Ys i)) (hindepX : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ) (hidentX : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hindepY : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Ys i) (Ys j) μ) (hidentY : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Ys i) (Ys 0) μ μ) (hindepZ : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (ChannelCoding.jointSequence Xs Ys i) (ChannelCoding.jointSequence Xs Ys j) μ) (hidentZ : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (ChannelCoding.jointSequence Xs Ys i) (ChannelCoding.jointSequence Xs Ys 0) μ μ) {ε : ℝ} (hε : 0 < ε) {η : ℝ} (hη : 0 < η) :

∃ (N : ℕ), ∀ n ≥ N, 1 - η ≤ (μ {ω : Ω | (jointRV Xs n ω, jointRV Ys n ω) ∈ ChannelCoding.jointlyTypicalSet μ Xs Ys n ε}).toReal

Joint asymptotic equipartition property (closed-form rate): for any ε, η > 0, there exists N such that for all n ≥ N, the jointly typical set has μ-measure ≥ 1 - η.

Used by

Closed-form `N(ε, η)` variants #

The _of_rate form (∃ N, ∀ n ≥ N, P) suffices for many callers. When the outer construction needs to substitute a sequence δ_n → 0 and conclude N(δ_n) ≤ n, N must instead be exposed as a closed-form function of the inputs.

The closed-form N is the same one extracted in the _of_rate proof bodies, hoisted out as a def. The _at_N theorems differ from _of_rate only in that the existential is collapsed to the explicit def.

noncomputable def

InformationTheory.Shannon.typicalSetMinN

(V η ε : ℝ) :

Closed-form N(V, η, ε) for typicalSet_prob_ge — extracted from the proof of typicalSet_prob_ge_of_rate.

Equations

InformationTheory.Shannon.typicalSetMinN V η ε = max 1 (⌈V / (η * ε ^ 2)⌉₊ + 1)

Instances For

Used by

theorem

InformationTheory.Shannon.typicalSetMinN_mono_V

{V V' η ε : ℝ} (hηε : 0 < η * ε ^ 2) (hVV' : V ≤ V') :

typicalSetMinN V η ε ≤ typicalSetMinN V' η ε

Used by

theorem

InformationTheory.Shannon.typicalSet_prob_ge_at_N

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [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 < ε) (hη : 0 < η) (n : ℕ) :

typicalSetMinN (pmfLogVariance μ Xs) η ε ≤ n → 1 - η ≤ (μ {ω : Ω | jointRV Xs n ω ∈ typicalSet μ Xs n ε}).toReal

Closed-form N version of typicalSet_prob_ge_of_rate.

Used by

theorem

InformationTheory.Shannon.typicalSet_prob_ge_at_N_le

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [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) μ μ) (V_upper : ℝ) (hV_upper : pmfLogVariance μ Xs ≤ V_upper) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) (n : ℕ) :

typicalSetMinN V_upper η ε ≤ n → 1 - η ≤ (μ {ω : Ω | jointRV Xs n ω ∈ typicalSet μ Xs n ε}).toReal

Variance-upper-bound version of typicalSet_prob_ge_at_N. The caller provides an upper bound V_upper ≥ pmfLogVariance μ Xs, and the closed-form N is typicalSetMinN V_upper η ε (independent of the true variance).

Used by

noncomputable def

InformationTheory.Shannon.expNegMulMinN

(g ε' : ℝ) :

Closed-form N(g, ε') for exponential decay exp(-n g) < ε'.

Equations

InformationTheory.Shannon.expNegMulMinN g ε' = ⌈max 0 (-Real.log ε' / g)⌉₊ + 1

Instances For

Used by

theorem

InformationTheory.Shannon.exp_neg_mul_lt_at_N

{g ε' : ℝ} (hg : 0 < g) (hε' : 0 < ε') (n : ℕ) :

expNegMulMinN g ε' ≤ n → Real.exp (-↑n * g) < ε'

Closed-form N version of exp_neg_mul_lt_of_rate.

Used by

theorem

InformationTheory.Shannon.channelCoding_E2_lt_at_N

{I R ε ε' : ℝ} (hgap : 0 < I - R - 3 * ε) (hε' : 0 < ε') (n : ℕ) :

expNegMulMinN (I - R - 3 * ε) ε' ≤ n → (↑⌈Real.exp (↑n * R)⌉₊ - 1) * Real.exp (↑n * (-I + 3 * ε)) < ε'

Closed-form N version of channelCoding_E2_lt_of_rate. The N is expNegMulMinN (I - R - 3ε) ε'.

Used by

noncomputable def

InformationTheory.Shannon.jointlyTypicalSetMinN

(V_X V_Y V_Z η ε : ℝ) :

Closed-form N(V_X, V_Y, V_Z, η, ε) for the joint AEP rate bound. Splits η/3 across three axes.

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

theorem

InformationTheory.Shannon.jointlyTypicalSet_prob_ge_at_N_le

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {β : Type u_3} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hYs : ∀ (i : ℕ), Measurable (Ys i)) (hindepX : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ) (hidentX : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hindepY : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Ys i) (Ys j) μ) (hidentY : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Ys i) (Ys 0) μ μ) (hindepZ : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (ChannelCoding.jointSequence Xs Ys i) (ChannelCoding.jointSequence Xs Ys j) μ) (hidentZ : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (ChannelCoding.jointSequence Xs Ys i) (ChannelCoding.jointSequence Xs Ys 0) μ μ) (V_X V_Y V_Z : ℝ) (hV_X : pmfLogVariance μ Xs ≤ V_X) (hV_Y : pmfLogVariance μ Ys ≤ V_Y) (hV_Z : pmfLogVariance μ (ChannelCoding.jointSequence Xs Ys) ≤ V_Z) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) (n : ℕ) :

jointlyTypicalSetMinN V_X V_Y V_Z η ε ≤ n → 1 - η ≤ (μ {ω : Ω | (jointRV Xs n ω, jointRV Ys n ω) ∈ ChannelCoding.jointlyTypicalSet μ Xs Ys n ε}).toReal

Variance-upper-bound version of joint AEP. The caller provides axis-wise variance upper bounds V_X, V_Y, V_Z, and the closed-form N is jointlyTypicalSetMinN V_X V_Y V_Z η ε.

Used by