InformationTheory.Shannon.ConditionalAEP

Imports 5

Conditional asymptotic equipartition for independent non-identical products #

A block zb : Fin n → T of symbols selects a per-coordinate observation law ν (zb i) on a finite alphabet β, and a per-coordinate statistic ψ (zb i). The empirical mean of the statistic concentrates around the ambient mean ∑ p, q p · (ν p)[ψ p] as soon as the empirical type of the block is close to q in total variation: Chebyshev on the product measure pins the empirical mean to its own conditional mean, and the type closeness pins that conditional mean to the ambient one.

The two halves are stated separately because their content is different: the Chebyshev half holds for every block, while the pin half is exactly what strong (rather than entropy-only) typicality of the block buys. The pin half amplifies the type radius by ∑ p, |(ν p)[ψ p]|, so a caller that needs the ambient deviation below ε must supply a block whose type radius is smaller than ε by that factor.

Main statements #

pi_nonuniform_mean_concentration — finite-n Chebyshev for a non-identically distributed independent product.
pi_nonuniform_concentration_tendsto — its uniform-in-(ν, ψ) form under a common sup-bound.
sum_eq_typeCount_mul — method-of-types regrouping of a per-coordinate sum.
abs_sum_mul_sub_sum_mul_le — the linear functional of a type is Lipschitz in the type.
pi_empiricalMean_deviation_le_of_type_close — the two halves combined.

Implementation notes #

The Chebyshev half takes the per-coordinate laws as a bare family ν : Fin n → Measure β, whereas the combined statement takes them as a kernel ν : T → Measure β read along a block; a caller that holds only a family, with no block to read it along, uses the former directly.

Chebyshev on a non-identically distributed product #

theorem

InformationTheory.Shannon.pi_nonuniform_mean_concentration

source

{β : Type u_2} [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] {n : ℕ} (hn : 0 < n) (ν : Fin n → MeasureTheory.Measure β) [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (ν i)] (ψ : Fin n → β → ℝ) {δ : ℝ} (hδ : 0 < δ) :

(MeasureTheory.Measure.pi ν).real {yb : Fin n → β | δ ≤ |(∑ i : Fin n, ψ i (yb i)) / ↑n - (∑ i : Fin n, ∫ (y : β), ψ i y ∂ν i) / ↑n|} ≤ (∑ i : Fin n, ProbabilityTheory.variance (ψ i) (ν i)) / (↑n ^ 2 * δ ^ 2)

Chebyshev's inequality for an independent, not identically distributed product: the mass the product Measure.pi ν puts on the blocks whose empirical mean of ψ deviates from the mean of the per-coordinate means by δ or more is at most (∑ i, variance (ψ i) (ν i)) / (n ^ 2 * δ ^ 2).

Used by

theorem

InformationTheory.Shannon.pi_nonuniform_concentration_tendsto

source

{β : Type u_2} [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] {B δ tol : ℝ} (hδ : 0 < δ) (htol : 0 < tol) :

∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (ν : Fin n → MeasureTheory.Measure β), (∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (ν i)) → ∀ (ψ : Fin n → β → ℝ), (∀ (i : Fin n) (y : β), |ψ i y| ≤ B) → (MeasureTheory.Measure.pi ν).real {yb : Fin n → β | δ ≤ |(∑ i : Fin n, ψ i (yb i)) / ↑n - (∑ i : Fin n, ∫ (y : β), ψ i y ∂ν i) / ↑n|} ≤ tol

The uniform form of the Chebyshev bound: past a threshold determined by the sup-bound B, the deviation δ and the tolerance tol alone, every independent non-identically distributed product of statistics bounded by B puts mass at most tol on the δ-deviation set of the empirical mean.

@audit:ok

Used by

Linear functionals of an empirical type #

theorem

InformationTheory.Shannon.sum_eq_typeCount_mul

source

{T : Type u_1} [Fintype T] [DecidableEq T] {n : ℕ} (z : Fin n → T) (f : T → ℝ) :

∑ i : Fin n, f (z i) = ∑ p : T, ↑(typeCount z p) * f p

Method-of-types regrouping: summing a statistic over the coordinates of a block equals summing it over the alphabet, each letter weighted by the number of coordinates carrying it.

Used by

theorem

InformationTheory.Shannon.abs_sum_mul_sub_sum_mul_le

source

{T : Type u_1} [Fintype T] [DecidableEq T] (t q g : T → ℝ) {r : ℝ} (hclose : ∀ (p : T), |t p - q p| ≤ r) :

|∑ p : T, t p * g p - ∑ p : T, q p * g p| ≤ (∑ p : T, |g p|) * r

The linear functional t ↦ ∑ p, t p * g p is Lipschitz in the coordinatewise distance of its argument, with constant ∑ p, |g p|.

Used by

The conditional AEP #

theorem

InformationTheory.Shannon.pi_empiricalMean_deviation_le_of_type_close

source

{T : Type u_1} {β : Type u_2} [Fintype T] [DecidableEq T] [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] {B ε tol : ℝ} (hε : 0 < ε) (htol : 0 < tol) :

∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (ν : T → MeasureTheory.Measure β), (∀ (p : T), MeasureTheory.IsProbabilityMeasure (ν p)) → ∀ (ψ : T → β → ℝ), (∀ (p : T) (y : β), |ψ p y| ≤ B) → ∀ (q : T → ℝ) (r : ℝ) (zb : Fin n → T), (∀ (p : T), |↑(typeCount zb p) / ↑n - q p| ≤ r) → (∑ p : T, |∫ (y : β), ψ p y ∂ν p|) * r < ε / 2 → (MeasureTheory.Measure.pi fun (i : Fin n) => ν (zb i)).real {yb : Fin n → β | ε ≤ |(∑ i : Fin n, ψ (zb i) (yb i)) / ↑n - ∑ p : T, q p * ∫ (y : β), ψ p y ∂ν p|} ≤ tol

For a block zb whose empirical type is within r of q, the product measure Measure.pi (fun i ↦ ν (zb i)) puts mass at most tol on the blocks whose empirical statistic deviates from the ambient mean ∑ p, q p · (ν p)[ψ p] by ε or more, once n ≥ N. The threshold N depends only on the sup-bound B, the deviation ε and the tolerance tol; the block, the type radius, the statistic and the kernel are quantified afterwards, so a caller may apply it uniformly over a code ensemble.

The hypothesis hpin is the radius separation: the type radius r must beat ε/2 after amplification by ∑ p, |(ν p)[ψ p]|. At r = ε the conclusion is false in general — the amplification constant is unrelated to ε — so a caller must shrink the type radius by that factor before invoking this. The reference vector q is arbitrary: the conclusion measures the deviation from q's own mean, so no consistency or full-support precondition on q arises here; a caller that wants the deviation read against an entropy supplies that identification itself.

@audit:ok

Used by