InformationTheory.Shannon.SMB.AlgoetCover.KMarkovApproximation
D.2 — k-Markov approximation #
InformationTheory.Shannon.pmfLogCondMarkov
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
(p : StationaryProcess μ α)
(k i : ℕ)
:
Ω → ℝ
k-Markov approximation to the per-step conditional log-likelihood:
for i ≤ k, use the genuine pmfLogCond μ p i; for i > k, use the
k-th conditional log-likelihood evaluated at the time-shifted point.
Equations
- InformationTheory.Shannon.pmfLogCondMarkov μ p k i ω = if i ≤ k then InformationTheory.Shannon.pmfLogCond μ p i ω else InformationTheory.Shannon.pmfLogCond μ p k (p.T^[i - k] ω)
Instances For
Used by
InformationTheory.Shannon.measurable_pmfLogCondMarkov
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
(p : StationaryProcess μ α)
(k i : ℕ)
:
Measurable (pmfLogCondMarkov μ p k i)
Measurability of pmfLogCondMarkov μ p k i.
Used by
InformationTheory.Shannon.pmfLogCondMarkov_sum_div_eq_add_birkhoffAverageReal
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
(p : StationaryProcess μ α)
(k : ℕ)
(ω : Ω)
{n : ℕ}
(hkn : k ≤ n)
:
(∑ i ∈ Finset.range (n + 1), pmfLogCondMarkov μ p k i ω) / (↑n + 1) = (∑ i ∈ Finset.range (k + 1), pmfLogCond μ p i ω - pmfLogCond μ p k ω) / (↑n + 1) + ↑(n - k + 1) / (↑n + 1) * birkhoffAverageReal p.T (pmfLogCond μ p k) (n - k) ω
Used by
InformationTheory.Shannon.birkhoffAverage_pmfLogCondMarkov_tendsto
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(p : ErgodicProcess μ α)
(k : ℕ)
:
∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto
(fun (n : ℕ) => (∑ i ∈ Finset.range (n + 1), pmfLogCondMarkov μ p.toStationaryProcess k i ω) / (↑n + 1))
Filter.atTop (nhds (conditionalEntropyTail μ p.toStationaryProcess k))
Cesàro average of the k-Markov approximation converges a.s. to
conditionalEntropyTail μ p k (Birkhoff applied to pmfLogCond μ p k).
Used by
InformationTheory.Shannon.negLogQk
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
(p : StationaryProcess μ α)
(k n : ℕ)
:
Ω → ℝ
Negative log-likelihood of the k-Markov approximation over the block of
length n.
Equations
- InformationTheory.Shannon.negLogQk μ p k n ω = ∑ i ∈ Finset.range n, InformationTheory.Shannon.pmfLogCondMarkov μ p k i ω
Instances For
Used by
InformationTheory.Shannon.negLogQk_div_tendsto_condEntropyTail
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(p : ErgodicProcess μ α)
(k : ℕ)
:
∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => negLogQk μ p.toStationaryProcess k n ω / ↑n) Filter.atTop
(nhds (conditionalEntropyTail μ p.toStationaryProcess k))
negLogQk μ p k n / n → conditionalEntropyTail μ p k a.s. as n → ∞.