InformationTheory.Shannon.SMB.AlgoetCover.TwoSidedRatio

Bridge: blockLogAvgZ n (natural extension of ω) = blockLogAvg n ω. The "natural extension" fun i : ℤ => p.obs i.toNat ω ignores negative coords (maps them to p.obs 0 ω = X ω), but blockLogAvgZ n only looks at coords {0, …, n-1}, where it agrees with forwardEmbed.

Used by

noncomputable def

InformationTheory.Shannon.negLogQInftyZ

source

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

(ℤ → α) → ℝ

Z-side negLogQ∞: Birkhoff sum of pmfLogCondInfty along the orbit.

Equations

InformationTheory.Shannon.negLogQInftyZ μ p n x = ∑ i ∈ Finset.range n, InformationTheory.Shannon.TwoSided.pmfLogCondInfty μ p (InformationTheory.Shannon.TwoSided.shiftZ ^[i] x)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.MRatioLowerZ

source

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

(ℤ → α) → ENNReal

The Z-side lower-bound likelihood ratio: exp(negLogQ∞ - n · blockLogAvgZ), which represents P_n/q_∞ lifted to ℝ≥0∞.

Equations

InformationTheory.Shannon.MRatioLowerZ μ p n x = ENNReal.ofReal (Real.exp (InformationTheory.Shannon.negLogQInftyZ μ p n x - ↑n * InformationTheory.Shannon.blockLogAvgZ μ p n x))

Instances For

Used by

noncomputable def

InformationTheory.Shannon.blockCondRatio

source

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

ℝ

Probability ratio at the (n+1)-block over the n-block: when P_n(s) > 0, this is P_{n+1}(snoc(s, a)) / P_n(s); defaulted to 0 when P_n(s) = 0.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.measurable_blockCondRatio_apply

source

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

Measurable fun (s : Fin n → α) => blockCondRatio μ p n s a

blockCondRatio is measurable (as a discrete map Fin n → α → α → ℝ).

Used by

theorem

InformationTheory.Shannon.firstBlockZ_singleton_pos_ae

source

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

∀ᵐ (x : ℤ → α) ∂TwoSided.μZ μ p, 0 < (MeasureTheory.Measure.map (firstBlockZ n) (TwoSided.μZ μ p)).real {firstBlockZ n x}

A.s. positivity of P_n^Z: the singleton mass at the realized firstBlockZ n x is a.s. positive under μZ.

Transferred from the Ω-side block_singleton_pos_ae_at via map_firstBlockZ_eq_map_blockRV.

Used by

theorem

InformationTheory.Shannon.MRatioLowerZ_succ_eq_mul

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (n : ℕ) (x : ℤ → α) (hPn_pos : 0 < (MeasureTheory.Measure.map (firstBlockZ n) (TwoSided.μZ μ p)).real {firstBlockZ n x}) (hPsucc_pos : 0 < (MeasureTheory.Measure.map (firstBlockZ (n + 1)) (TwoSided.μZ μ p)).real {firstBlockZ (n + 1) x}) :

MRatioLowerZ μ p (n + 1) x = MRatioLowerZ μ p n x * ENNReal.ofReal (blockCondRatio μ p n (firstBlockZ n x) (x ↑n)) * ENNReal.ofReal (Real.exp (TwoSided.pmfLogCondInfty μ p (TwoSided.shiftZ ^[n] x)))

Pointwise factorization of MRatioLowerZ (n+1) on the a.s. positive set.

On the set where both P_n(firstBlockZ n x) > 0 and P_{n+1}(firstBlockZ (n+1) x) > 0, we have the decomposition MRatioLowerZ (n+1) x = MRatioLowerZ n x · ofReal(blockCondRatio · exp(pmfLogCondInfty(shift^n x))), where blockCondRatio is the chain-rule ratio.

Used by

theorem

InformationTheory.Shannon.lintegral_mul_eq_lintegral_mul_condLExp

source

{Ω : Type u_3} {m₀ m : MeasurableSpace Ω} (hm : m ≤ m₀) (μ : MeasureTheory.Measure Ω) [MeasureTheory.SigmaFinite (μ.trim hm)] {g : Ω → ENNReal} (hg : Measurable g) {f : Ω → ENNReal} (hf : Measurable f) :

∫⁻ (x : Ω), g x * f x ∂μ = ∫⁻ (x : Ω), g x * μ⁻[f | m] x ∂μ

ENNReal pull-out (general): for g : Ω → ℝ≥0∞ m-measurable and f : Ω → ℝ≥0∞ measurable, ∫⁻ x, g · f dμ = ∫⁻ x, g · μ⁻[f|m] dμ.

Used by

def

InformationTheory.Shannon.shiftedPastSigma

source

@[reducible]

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

MeasurableSpace (ℤ → α)

σ-algebra of the shifted past: events depending only on {x_i : i ≤ n - 1}.

Equations

InformationTheory.Shannon.shiftedPastSigma n = MeasurableSpace.comap InformationTheory.Shannon.TwoSided.shiftZ ^[n] InformationTheory.Shannon.TwoSided.negPastSigma

Instances For

Used by

theorem

InformationTheory.Shannon.shiftedPastSigma_le

source

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

shiftedPastSigma n ≤ MeasurableSpace.pi

Used by

theorem

InformationTheory.Shannon.measurable_condProbInfty_comp_shift_shiftedPastSigma

source

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

Measurable fun (x : ℤ → α) => TwoSided.condProbInfty μ p a (TwoSided.shiftZ ^[n] x)

The map condProbInfty(a) ∘ shift^[n] is measurable w.r.t. shiftedPastSigma n.

Used by

theorem

InformationTheory.Shannon.measurable_shiftedPastSigma_of_eq_comp

source

{α : Type u_2} [MeasurableSpace α] {β : Type u_3} [MeasurableSpace β] (n : ℕ) (f : (ℤ → α) → β) {g : (ℤ → α) → β} (hg : Measurable g) (hf : f = g ∘ TwoSided.shiftZ ^[n]) :

Measurable f

Generic comap-through-shift lemma: if f : (∀_:ℤ,α) → β satisfies f = g ∘ shiftZ^[n] for some negPastSigma-measurable g, then f is shiftedPastSigma n-measurable.

Used by

theorem

InformationTheory.Shannon.measurable_coord_negPastSigma

source

{α : Type u_2} [MeasurableSpace α] {k : ℤ} (hk : k ≤ -1) :

Measurable fun (y : ℤ → α) => y k

Coordinate projection (· k) is negPastSigma-measurable when k ≤ -1.

Used by

theorem

InformationTheory.Shannon.measurable_MRatioLowerZ_shiftedPastSigma

source

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

Measurable (MRatioLowerZ μ p n)

MRatioLowerZ μ p n is shiftedPastSigma n-measurable. Depends only on x_0, …, x_{n-1}, which after shift^n lives at indices -n, …, -1.

Used by

theorem

InformationTheory.Shannon.condLExp_indicator_coord_n_eq_ofReal_condProbInfty_shift

source

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

(fun (x : ℤ → α) => ENNReal.ofReal (TwoSided.condProbInfty μ p a (TwoSided.shiftZ ^[n] x))) =ᵐ[TwoSided.μZ μ p] (TwoSided.μZ μ p)⁻[(TwoSided.shiftZ ^[n] ⁻¹' TwoSided.coord0 ⁻¹' {a}).indicator fun (x : ℤ → α) => 1 | shiftedPastSigma n]

Substep A — Tower identification: the conditional Lebesgue expectation of the ENNReal indicator 1_{x_n = a} w.r.t. shiftedPastSigma n equals ofReal(condProbInfty(a)(shift^n x)) a.s.

Proof: by uniqueness of conditional Lebesgue expectation (ae_eq_condLExp). The candidate is shiftedPastSigma n-measurable, and its integral on each s = (shift^n)⁻¹' t matches the indicator's integral. The latter reduces (via MeasurePreserving.setLIntegral_comp_preimage) to a real-valued condExp identity setIntegral_condExp for condProbInfty(a), converted to ENNReal via integral_eq_lintegral_of_nonneg_ae + finiteness.

Used by

theorem

InformationTheory.Shannon.indicator_mul_ofReal_exp_pmf_eq

source

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

(TwoSided.shiftZ ^[n] ⁻¹' TwoSided.coord0 ⁻¹' {a}).indicator (fun (x : ℤ → α) => 1) x * ENNReal.ofReal (Real.exp (TwoSided.pmfLogCondInfty μ p (TwoSided.shiftZ ^[n] x))) = (TwoSided.shiftZ ^[n] ⁻¹' TwoSided.coord0 ⁻¹' {a}).indicator (fun (x : ℤ → α) => 1) x * ENNReal.ofReal (Real.exp (-Real.log (TwoSided.condProbInfty μ p a (TwoSided.shiftZ ^[n] x))))

Indicator-support collapse: on the set {x_n = a}, the factor exp(pmfLogCondInfty(shift^n x)) equals 1/condProbInfty(a)(shift^n x) (in ℝ; with 1/0 = 0). Formulated as an indicator-times-factor pointwise identity.

Used by

theorem