InformationTheory.Shannon.LZ78.ZivCondContext

Imports 6

LZ78 conditional-context sub-distribution (node-context route) #

This file supplies the first measure-theoretic atom of the conditional-context route for the LZ78 achievability bound ziv_aseventual_le_blockLogAvg₂ (LZ78/AsymptoticOptimality/ParentBridgeAchievability.lean).

Background #

The two simple grouping routes are ruled out: node-position grouping (the overhead trap) and marginal-length grouping (ZivMeasureBridge.lean, the direction is wrong since ∑ -log P_marginal ≥ -log Pₙ for sources with memory). The surviving structure is the conditional sub-distribution q(symbol | context), which reaches -log Pₙ via the chain rule. The first building block of that route is the per-context (fixed-tuple) conditional sub-distribution ∑_a q(v · a | v) ≤ 1.

Main definitions #

condContextProb — the fixed-tuple conditional probability q(v, a) = P(blockRV (m+1) = Fin.snoc v a) / P(blockRV m = v), the ω-independent node-context conditional (NOT the path-prefix condPhraseProb, which is observation-dependent and a dead start).

Main statements #

sum_extend_marginal_real_eq — Kolmogorov consistency, ∑_a P(blockRV (m+1) = Fin.snoc v a) = P(blockRV m = v). The first m coordinates of blockRV (m+1) are blockRV m, so the events {blockRV (m+1) = snoc v a} partition {blockRV m = v} disjointly over a.
condContext_sum_eq_one / condContext_sum_le_one — the per-context conditional masses sum to 1 (resp. ≤ 1) when 0 < P(blockRV m = v). This is the sub-distribution input the conditional log-sum step consumes.
condContext_card_mul_log_le_sum_neg_log — per-context log-sum step: card S · log (card S) ≤ ∑_{a ∈ S} -log q(v, a) for a set S of symbols with positive conditional masses; the conditional analogue of group_card_mul_log_le_sum_neg_log (ZivMeasureBridge.lean).

Step 1 — Kolmogorov consistency of the extended marginal #

theorem

InformationTheory.Shannon.blockRV_succ_preimage_snoc

source

{α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (p : StationaryProcess μ α) (m : ℕ) (v : Fin m → α) (a : α) :

p.blockRV (m + 1) ⁻¹' {Fin.snoc v a} = {ω : Ω | p.blockRV m ω = v ∧ p.obs m ω = a}

The block-extension fibre identity (unconditional): for a fixed tuple v : Fin m → α and symbol a, the preimage of the extended cylinder {blockRV (m+1) = Fin.snoc v a} is exactly the set of ω whose m-block is v and whose time-m observation is a.

Used by

theorem

InformationTheory.Shannon.blockRV_succ_preimage_iUnion_eq

source

{α : Type u_1} {Ω : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (p : StationaryProcess μ α) (m : ℕ) (v : Fin m → α) :

⋃ a ∈ Finset.univ, p.blockRV (m + 1) ⁻¹' {Fin.snoc v a} = p.blockRV m ⁻¹' {v}

Over the symbol a, the extended-cylinder preimages {blockRV (m+1) = Fin.snoc v a} partition the m-block cylinder {blockRV m = v}.

Used by

theorem

InformationTheory.Shannon.sum_extend_marginal_real_eq

source

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

∑ a : α, (MeasureTheory.Measure.map (p.blockRV (m + 1)) μ).real {Fin.snoc v a} = (MeasureTheory.Measure.map (p.blockRV m) μ).real {v}

Kolmogorov consistency (unconditional): the extended length-m+1 marginals over the last symbol sum to the length-m marginal, ∑_a P(blockRV (m+1) = Fin.snoc v a) = P(blockRV m = v). The first m coordinates of blockRV (m+1) agree with blockRV m, so the extended cylinders form a disjoint partition of the m-block cylinder; finite additivity of the pushforward gives the identity. This is the conditional analogue of the marginal sub-distribution sum_marginal_real_le_one (ZivMeasureBridge.lean).

Used by

theorem

InformationTheory.Shannon.sum_extend_marginal_real_le

source

∑ a : α, (MeasureTheory.Measure.map (p.blockRV (m + 1)) μ).real {Fin.snoc v a} ≤ (MeasureTheory.Measure.map (p.blockRV m) μ).real {v}

A ≤ form of consistency for the extended marginal, the input the per-context log-sum step needs.

Used by

Step 2 — conditional sub-distribution #

noncomputable def

InformationTheory.Shannon.condContextProb

source

{α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (p : StationaryProcess μ α) {m : ℕ} (v : Fin m → α) (a : α) :

ℝ

The fixed-tuple conditional probability q(v, a) (node-context, ω-independent): the conditional mass of the extended block Fin.snoc v a given the context block v, q(v, a) = P(blockRV (m+1) = Fin.snoc v a) / P(blockRV m = v).

This is the conditional q(symbol | context) the LZ78 achievability chain rule requires — NOT the path-prefix ratio condPhraseProb, which is observation-dependent and a dead start (∑ⱼ qⱼ ≈ c).

Equations

InformationTheory.Shannon.condContextProb μ p v a = (MeasureTheory.Measure.map (p.blockRV (m + 1)) μ).real {Fin.snoc v a} / (MeasureTheory.Measure.map (p.blockRV m) μ).real {v}

Instances For

Used by

theorem

InformationTheory.Shannon.condContext_sum_eq_one

source

∑ a : α, condContextProb μ p v a = 1

When the context mass P(blockRV m = v) is strictly positive, the conditional masses sum to 1. Immediate from Kolmogorov consistency sum_extend_marginal_real_eq.

Used by

theorem

InformationTheory.Shannon.condContext_sum_le_one

source

∑ a : α, condContextProb μ p v a ≤ 1

The per-context sub-distribution bound ∑_a q(v · a | v) ≤ 1: the node-context conditional sub-distribution. This is the missing measure-theoretic piece the conditional log-sum step consumes (the third quantity, neither marginal nor path-prefix).

Used by

Step 3 — per-context log-sum step #

theorem

InformationTheory.Shannon.condContext_card_mul_log_le_sum_neg_log

source

{α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (p : StationaryProcess μ α) {m : ℕ} (v : Fin m → α) (S : Finset α) (hPpos : ∀ a ∈ S, 0 < condContextProb μ p v a) (hPsum : ∑ a ∈ S, condContextProb μ p v a ≤ 1) :

↑S.card * Real.log ↑S.card ≤ ∑ a ∈ S, -Real.log (condContextProb μ p v a)

The per-context log-sum step: for a finite set S of symbols with strictly positive conditional masses q(v, a) > 0 whose masses sum to at most 1,

card S · log (card S) ≤ ∑_{a ∈ S} -log q(v, a).

The conditional analogue of group_card_mul_log_le_sum_neg_log (ZivMeasureBridge.lean); log_sum_inequality with aᵢ ≡ 1, bᵢ = q(v, aᵢ).

Used by

Step 4 — symbol-by-symbol chain rule (conditional route reaches -log Pₙ) #

theorem

InformationTheory.Shannon.blockRV_succ_eq_snoc

source

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

p.blockRV (m + 1) ω = Fin.snoc (p.blockRV m ω) (p.obs m ω)

Pointwise block-extension: blockRV (m+1) ω = Fin.snoc (blockRV m ω) (obs m ω).

Used by

theorem

InformationTheory.Shannon.condContextProb_path_eq_ratio

source

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

condContextProb μ p (p.blockRV m ω) (p.obs m ω) = prefixBlockProb μ p ω (m + 1) / prefixBlockProb μ p ω m

Per-step identity: the node-context conditional along the path equals the ratio of successive prefix block probabilities, condContextProb μ p (blockRV m ω) (obs m ω) = prefixBlockProb (m+1) / prefixBlockProb m.

Used by

theorem

InformationTheory.Shannon.prod_condContextProb_path_telescope

source

{α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (n : ℕ) (ω : Ω) (hpos : ∀ m ≤ n, prefixBlockProb μ p ω m ≠ 0) :

∏ m ∈ Finset.range n, condContextProb μ p (p.blockRV m ω) (p.obs m ω) = prefixBlockProb μ p ω n

Symbol-by-symbol chain-rule telescoping (equality): the per-path block probability factorizes as the product of node-context conditionals along the path, given positivity of the intermediate prefix masses.

Used by

theorem

InformationTheory.Shannon.sum_neg_log_condContextProb_path_eq

source

∑ m ∈ Finset.range n, -Real.log (condContextProb μ p (p.blockRV m ω) (p.obs m ω)) = -Real.log ((MeasureTheory.Measure.map (p.blockRV n) μ).real {p.blockRV n ω})

The conditional chain rule reaches -log Pₙ (equality): unlike the marginal route (direction-mismatched), the node-context conditional sum reaches the block neg-log-probability exactly, ∑_{m<n} -log q_cond = -log Pₙ{block ω}.

Used by

theorem

InformationTheory.Shannon.sum_neg_log_condContextProb_path_eq_blockLogAvg

source

{α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) {n : ℕ} (hn : 0 < n) (ω : Ω) (hpos : ∀ m ≤ n, prefixBlockProb μ p ω m ≠ 0) :

∑ m ∈ Finset.range n, -Real.log (condContextProb μ p (p.blockRV m ω) (p.obs m ω)) = ↑n * blockLogAvg μ p n ω

The conditional chain rule equals n · blockLogAvg (equality): the SMB-controlled quantity. Combined with SMB (blockLogAvg → entropyRate), this connects the conditional-context route to the source entropy limit.

Used by