Skip to content

InformationTheory.Probability.TwoSidedExtension.Backward

Imports 18

Forward filtration of the finite past + `pmfLogCond` Lévy convergence #

The forward filtration is the monotone (in ℕ) family of σ-algebras pastSigma k of events depending only on the finite past {coord_i : -k ≤ i ≤ -1} of length k. As k → ∞, the filtration's ⨆-limit is the σ-algebra cylinderEvents {i : ℤ | i ≤ -1} of the infinite negative past.

This is the shape needed by MeasureTheory.Integrable.tendsto_ae_condExp (forward Lévy upward convergence): if g is (⨆ k, ℱ k)-strongly measurable and integrable, then μ[g | ℱ k] → g a.s.

For each a : α, the real-valued process condProbPast a k := μZ[ (coord0 ⁻¹' {a}).indicator (1 : (ℤ→α)→ℝ) | pastFiltration k ] is a martingale (via martingale_condExp). The infinite-past conditional probability condProbInfty a is defined directly as the conditional expectation with respect to ⨆ k, pastFiltration k; forward Lévy then gives condProbPast a k → condProbInfty a a.s.

The per-step conditional log-likelihood is then pmfLogCondPast k ω := -log ( ∑ a, indicator(coord0 ω = a) * condProbPast a k ω ), which collapses pointwise to -log condProbPast (coord0 ω) k ω.

The terminal integral identity ∫ pmfLogCondInfty dμZ = entropyRate μ p follows from the per-step identity ∫ pmfLogCondPast k dμZ = conditionalEntropyTail μ p k (via the joint-law equality of shiftedMarginal) and DCT pushed through forward Lévy + entropyRate_eq_lim_condEntropy.

def

InformationTheory.Shannon.TwoSided.pastSigma

@[reducible]

{α : Type u_2} [MeasurableSpace α] (k : ℕ) :

MeasurableSpace (ℤ → α)

The σ-algebra of events depending only on the finite past {coord_i : -k ≤ i ≤ -1} of length k. For k = 0 this is the trivial σ-algebra (the set {i | 0 ≤ i ∧ i ≤ -1} is empty).

Equations

InformationTheory.Shannon.TwoSided.pastSigma k = MeasureTheory.cylinderEvents {i : ℤ | -↑k ≤ i ∧ i ≤ -1}

Instances For

Used by

theorem

InformationTheory.Shannon.TwoSided.pastSigma_mono

{α : Type u_2} [MeasurableSpace α] :

Monotone pastSigma

pastSigma is monotone in k (longer past = larger σ-algebra).

Used by

def

InformationTheory.Shannon.TwoSided.pastFiltration

{α : Type u_2} [MeasurableSpace α] :

MeasureTheory.Filtration ℕ MeasurableSpace.pi

The forward past filtration on ℕ: pastFiltration k is pastSigma k, the σ-algebra of events depending on the finite past {coord_i : -k ≤ i ≤ -1}.

Equations

InformationTheory.Shannon.TwoSided.pastFiltration = { seq := fun (k : ℕ) => InformationTheory.Shannon.TwoSided.pastSigma k, mono' := ⋯, le' := ⋯ }

Instances For

Used by

theorem

InformationTheory.Shannon.TwoSided.pastFiltration_apply

@[simp]

{α : Type u_2} [MeasurableSpace α] (k : ℕ) :

↑pastFiltration k = pastSigma k

Used by

def

InformationTheory.Shannon.TwoSided.negPastSigma

@[reducible]

{α : Type u_2} [MeasurableSpace α] :

MeasurableSpace (ℤ → α)

The σ-algebra of events depending on the infinite negative past {coord_i : i ≤ -1}. This is ⨆ k, pastSigma k.

Equations

InformationTheory.Shannon.TwoSided.negPastSigma = MeasureTheory.cylinderEvents {i : ℤ | i ≤ -1}

Instances For

Used by

theorem

InformationTheory.Shannon.TwoSided.iSup_pastSigma_eq_negPastSigma

{α : Type u_2} [MeasurableSpace α] :

⨆ (k : ℕ), pastSigma k = negPastSigma

The supremum of the forward past filtration is the infinite negative past σ-algebra.

Unfolds cylinderEvents as ⨆ i ∈ Δ, (m i).comap (· i) and rearranges the nested iSups: for any i ≤ -1, i ∈ [-k, -1] for k := (-i).toNat.

Used by

def

InformationTheory.Shannon.TwoSided.coord0

{α : Type u_2} :

(ℤ → α) → α

The coordinate-0 evaluation.

Equations

InformationTheory.Shannon.TwoSided.coord0 x = x 0

Instances For

Used by

theorem

InformationTheory.Shannon.TwoSided.measurable_coord0

{α : Type u_2} [MeasurableSpace α] :

Measurable coord0

The coordinate-0 map is measurable.

Used by

theorem

InformationTheory.Shannon.TwoSided.indicator_coord0_eq_le_one

{α : Type u_2} (a : α) (x : ℤ → α) :

(coord0 ⁻¹' {a}).indicator (fun (x : ℤ → α) => 1) x ≤ 1

The indicator of {coord0 = a} is bounded by 1.

Used by

theorem

InformationTheory.Shannon.TwoSided.indicator_coord0_eq_nonneg

{α : Type u_2} (a : α) (x : ℤ → α) :

0 ≤ (coord0 ⁻¹' {a}).indicator (fun (x : ℤ → α) => 1) x

The indicator of {coord0 = a} is nonneg.

Used by

theorem

InformationTheory.Shannon.TwoSided.measurableSet_coord0_eq

{α : Type u_2} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) :

MeasurableSet (coord0 ⁻¹' {a})

The set {coord0 = a} is measurable.

Used by

theorem

InformationTheory.Shannon.TwoSided.integrable_indicator_coord0_eq

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (a : α) :

MeasureTheory.Integrable ((coord0 ⁻¹' {a}).indicator fun (x : ℤ → α) => 1) (μZ μ p)

The indicator function (coord0 ⁻¹' {a}).indicator 1 is integrable under μZ.

Used by

noncomputable def

InformationTheory.Shannon.TwoSided.condProbPast

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (a : α) (k : ℕ) :

(ℤ → α) → ℝ

The real-valued forward conditional probability of {coord0 = a} given the finite past pastFiltration k, viewed as a function on ℤ → α.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.TwoSided.martingale_condProbPast

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (a : α) :

MeasureTheory.Martingale (fun (k : ℕ) => (μZ μ p)[(coord0 ⁻¹' {a}).indicator fun (x : ℤ → α) => 1 | ↑pastFiltration k]) pastFiltration (μZ μ p)

For each a : α, condProbPast a is a (forward) martingale w.r.t. the past filtration.

Used by

noncomputable def

InformationTheory.Shannon.TwoSided.condProbInfty

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (a : α) :

(ℤ → α) → ℝ

The infinite-past conditional probability of {coord0 = a} given ⨆ k, pastFiltration k.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.TwoSided.condProbPast_tendsto_condProbInfty

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (a : α) :

∀ᵐ (x : ℤ → α) ∂μZ μ p, Filter.Tendsto (fun (k : ℕ) => condProbPast μ p a k x) Filter.atTop (nhds (condProbInfty μ p a x))

Forward Lévy upward convergence: condProbPast a k → condProbInfty a a.s. as k → ∞. Direct application of MeasureTheory.Integrable.tendsto_ae_condExp (Lévy's upward theorem).

Used by

theorem

InformationTheory.Shannon.TwoSided.integrable_condProbPast

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (a : α) (k : ℕ) :

MeasureTheory.Integrable (condProbPast μ p a k) (μZ μ p)

condProbPast a k is integrable.

Used by

theorem

InformationTheory.Shannon.TwoSided.stronglyMeasurable_condProbPast

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (a : α) (k : ℕ) :

MeasureTheory.StronglyMeasurable (condProbPast μ p a k)

condProbPast a k is strongly measurable w.r.t. pastFiltration k.

Used by

theorem

InformationTheory.Shannon.TwoSided.stronglyMeasurable_condProbInfty

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (a : α) :

MeasureTheory.StronglyMeasurable (condProbInfty μ p a)

condProbInfty a is ⨆ k, pastFiltration k-strongly measurable.

Used by

theorem

InformationTheory.Shannon.TwoSided.ae_zero_le_condProbPast

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (a : α) (k : ℕ) :

0 ≤ᵐ[μZ μ p] condProbPast μ p a k

condProbPast a k ≥ 0 a.s.

Used by

theorem

InformationTheory.Shannon.TwoSided.ae_condProbPast_le_one

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (a : α) (k : ℕ) :

condProbPast μ p a k ≤ᵐ[μZ μ p] fun (x : ℤ → α) => 1

condProbPast a k ≤ 1 a.s.

Used by

theorem

InformationTheory.Shannon.TwoSided.ae_zero_le_condProbInfty

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (a : α) :

0 ≤ᵐ[μZ μ p] condProbInfty μ p a

condProbInfty a ≥ 0 a.s.

Used by

theorem

InformationTheory.Shannon.TwoSided.ae_condProbInfty_le_one

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (a : α) :

condProbInfty μ p a ≤ᵐ[μZ μ p] fun (x : ℤ → α) => 1

condProbInfty a ≤ 1 a.s.

Used by

theorem

InformationTheory.Shannon.TwoSided.condProbInfty_eq_condExp_tail

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (a : α) :

condProbInfty μ p a =ᵐ[μZ μ p] (μZ μ p)[(coord0 ⁻¹' {a}).indicator fun (x : ℤ → α) => 1 | ⨆ (n : ℕ), ↑pastFiltration n]

condProbInfty a is by definition the conditional expectation of the indicator 1_{coord0=a} w.r.t. the σ-algebra ⨆ k, pastFiltration k of the infinite past.

Used by

noncomputable def

InformationTheory.Shannon.TwoSided.pmfLogCondPast

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (k : ℕ) :

(ℤ → α) → ℝ

Per-step conditional log-likelihood under μZ conditioned on pastSigma k.

Defined as -log (∑ a, indicator(coord0 = a) * condProbPast a k). On the full-measure set where the conditional probability of the actual coord0 value is positive, this is -log condProbPast (coord0 x) k x.

Equations

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

Instances For

Used by

noncomputable def

InformationTheory.Shannon.TwoSided.pmfLogCondInfty

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) :

(ℤ → α) → ℝ

Limit log-likelihood (conditional on the full backward tail).

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.TwoSided.pmfLogCondPast_inner_eq_self

{α : Type u_2} [Fintype α] (f : α → ℝ) (x : ℤ → α) :

∑ a : α, (coord0 ⁻¹' {a}).indicator (fun (x : ℤ → α) => 1) x * f a = f (coord0 x)

Per-step (and limit) inner sum simplifies to a single conditional probability of the realized coord-0 value.

Used by