Entropy rate

The conditional entropy pastCondEntropy X μ n of the value of a process at time n given the n values before it falls as the past grows when the process is stationary, and its infimum is the entropy rate. The drop from a past of t - 1 values to a past of t is the information distanceInfo X μ t that the value at time 0 carries about the value at time t given the values between them. The entropy rate plus the information at distances beyond T is the conditional entropy given a past of T values.

Main definitions

• InformationTheory.pastCondEntropy X μ n: the entropy of X n given X 0, …, X (n - 1).
• InformationTheory.distanceInfo X μ t: the mutual information of X t and X 0 given the values between them.
• InformationTheory.entropyRate X μ: the infimum of pastCondEntropy X μ.

Main statements

• InformationTheory.entropy_block: the chain rule for a block.
• InformationTheory.distanceInfo_succ: under stationarity, distanceInfo X μ (t + 1) is the drop from pastCondEntropy X μ t to pastCondEntropy X μ (t + 1).
• InformationTheory.entropyRate_add_tsum: under stationarity, the entropy rate plus the information at distances beyond T is pastCondEntropy X μ T.

References

• [CT06]
• [HDF21]

noncomputable def InformationTheory.pastCondEntropy {Ω : Type u_1} {S : Type u_2} [MeasurableSpace Ω] [MeasurableSpace S] (X : ℕ → Ω → S) (μ : MeasureTheory.Measure Ω) (n : ℕ) : ℝ

pastCondEntropy X μ n is the conditional entropy of the value at time n given the n values before it.

Equations

• InformationTheory.pastCondEntropy X μ n = InformationTheory.condEntropy (X n) (ProbabilityTheory.block X 0 n) μ

noncomputable def InformationTheory.distanceInfo {Ω : Type u_1} {S : Type u_2} [MeasurableSpace Ω] [MeasurableSpace S] (X : ℕ → Ω → S) (μ : MeasureTheory.Measure Ω) (t : ℕ) : ℝ

distanceInfo X μ t is the mutual information I[X t : X 0 | X 1, …, X (t - 1)] between values at distance t given the values between them, which is the entropy of X t that X 0 removes.

Equations

• InformationTheory.distanceInfo X μ t = InformationTheory.condEntropy (X t) (ProbabilityTheory.block X 1 (t - 1)) μ - InformationTheory.condEntropy (X t) (ProbabilityTheory.block X 0 t) μ

noncomputable def InformationTheory.entropyRate {Ω : Type u_1} {S : Type u_2} [MeasurableSpace Ω] [MeasurableSpace S] (X : ℕ → Ω → S) (μ : MeasureTheory.Measure Ω) : ℝ

The entropy rate is the infimum of the conditional entropies of a value given its past, which is their limit when the process is stationary.

Equations

• InformationTheory.entropyRate X μ = ⨅ (n : ℕ), InformationTheory.pastCondEntropy X μ n

theorem InformationTheory.pastCondEntropy_zero {Ω : Type u_1} {S : Type u_2} [MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] {X : ℕ → Ω → S} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hX : ∀ (t : ℕ), Measurable (X t)) : pastCondEntropy X μ 0 = entropy (X 0) μ

With no past, the conditional entropy is the entropy of the first value.

theorem InformationTheory.distanceInfo_succ_nonneg {Ω : Type u_1} {S : Type u_2} [MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] {X : ℕ → Ω → S} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hX : ∀ (t : ℕ), Measurable (X t)) (t : ℕ) : 0 ≤ distanceInfo X μ (t + 1)

Conditioning on a further value of the past never adds entropy, so distanceInfo X μ (t + 1) is nonnegative.

theorem InformationTheory.entropy_block {Ω : Type u_1} {S : Type u_2} [MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] {X : ℕ → Ω → S} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hX : ∀ (t : ℕ), Measurable (X t)) (T : ℕ) : entropy (ProbabilityTheory.block X 0 T) μ = ∑ t ∈ Finset.range T, pastCondEntropy X μ t

The entropy of a block is the sum of the conditional entropies of its values given their predecessors.

theorem InformationTheory.distanceInfo_succ {Ω : Type u_1} {S : Type u_2} [MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] {X : ℕ → Ω → S} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hX : ∀ (t : ℕ), Measurable (X t)) (hs : ProbabilityTheory.IsStationary X μ) (t : ℕ) : distanceInfo X μ (t + 1) = pastCondEntropy X μ t - pastCondEntropy X μ (t + 1)

Under stationarity, distanceInfo X μ (t + 1) is the drop in conditional entropy as the past grows from t values to t + 1.

theorem InformationTheory.pastCondEntropy_antitone {Ω : Type u_1} {S : Type u_2} [MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] {X : ℕ → Ω → S} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hX : ∀ (t : ℕ), Measurable (X t)) (hs : ProbabilityTheory.IsStationary X μ) : Antitone (pastCondEntropy X μ)

theorem InformationTheory.sum_Icc_mul_distanceInfo {Ω : Type u_1} {S : Type u_2} [MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] {X : ℕ → Ω → S} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hX : ∀ (t : ℕ), Measurable (X t)) (hs : ProbabilityTheory.IsStationary X μ) (T : ℕ) : ∑ t ∈ Finset.Icc 1 T, ↑t * distanceInfo X μ t = ∑ t ∈ Finset.range T, pastCondEntropy X μ t - ↑T * pastCondEntropy X μ T

The weighted sum of the information at distances up to T, by summation by parts.

theorem InformationTheory.tendsto_pastCondEntropy {Ω : Type u_1} {S : Type u_2} [MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] {X : ℕ → Ω → S} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hX : ∀ (t : ℕ), Measurable (X t)) (hs : ProbabilityTheory.IsStationary X μ) : Filter.Tendsto (pastCondEntropy X μ) Filter.atTop (nhds (entropyRate X μ))

theorem InformationTheory.entropyRate_add_tsum {Ω : Type u_1} {S : Type u_2} [MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] {X : ℕ → Ω → S} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hX : ∀ (t : ℕ), Measurable (X t)) (hs : ProbabilityTheory.IsStationary X μ) (T : ℕ) : entropyRate X μ + ∑' (t : ℕ), distanceInfo X μ (T + t + 1) = pastCondEntropy X μ T

The entropy rate plus the information at distances beyond T is the conditional entropy of a value given the T values before it.