InformationTheory

InformationTheory.Shannon.LZ78.ZivCondGrouping

source

Imports 7

LZ78 conditional (k-state, length) grouping bridge #

This file supplies the conditional analogue of the length-grouping measure bridge for the LZ78 achievability bound ziv_aseventual_le_blockLogAvg₂ (LZ78/AsymptoticOptimality/ParentBridgeAchievability.lean), via the markovFactor route.

Approach #

The dead marginal route (ZivMeasureBridge.lean, lz78PhraseStrings_mul_log_le_sum_neg_log_marginal_add_overhead) fibers phrases by List.length and lower-bounds the entropy by ∑ -log P_ℓ for the marginal P_ℓ. That direction is dead (the marginal sum bound runs the wrong way for the Ziv connection). This file instead uses the conditional per-k-state product sub-distribution condQkState μ p k s (from markovFactor) as the grouping vehicle, fibering phrases by the pair (k-state, length):

  1. Group over ι = (Fin k → α) × ℕ: apply card_mul_log_le_sum_group_mul_log_add_card_log to the image G = phrases.image (st w, w.length), giving c · log c ≤ ∑_g c_g · log c_g + c · log (G.card), where the fibers grp g = phrases.filter (st w, w.length) = g partition phrases.

  2. Apply the per-fiber log-sum step: within a fiber (s, ℓ), all phrases have length ℓ, so toFinVec ℓ injects them into Fin ℓ → α. With P Z = (condQkState μ p k s ℓ Z).toReal, group_card_mul_log_le_sum_neg_log gives card · log card ≤ ∑ -log P.

    • The .toReal sub-distribution bound ∑_{Z} P Z ≤ 1 is derived from the ℝ≥0∞ fact condQkState_sum_le_one via ENNReal.toReal_sum (each term is ≤ 1 < ⊤, so finite) and ENNReal.toReal_mono. This is the route's .toReal bridge (iii).

  3. Aggregate: sum the per-fiber bounds back into a single sum over phrases.

The result condState_grouping_bound is stated abstractly (a Finset (List α) of phrases with an arbitrary k-state assignment st); wiring it to the actual LZ78 parse structure is a downstream leg.

Per-element bound and finiteness for condQkState #

theorem

InformationTheory.Shannon.condQkState_le_one

source
{α : Type u_1} {Ω : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (k : ℕ) (s : Fin k → α) (ℓ : ℕ) (Z : Fin ℓ → α) :
condQkState μ p k s ℓ Z ≤ 1

Each conditional mass condQkState μ p k s ℓ Z is at most 1: a single summand is bounded by the total ≤ 1 sub-distribution sum.

Used by

    The .toReal sub-distribution bridge (route step iii) #

    theorem

    InformationTheory.Shannon.sum_condQkState_toReal_le_one

    source
    {α : Type u_1} {Ω : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (k : ℕ) (s : Fin k → α) (ℓ : ℕ) (S : Finset (Fin ℓ → α)) :
    ∑ Z ∈ S, (condQkState μ p k s ℓ Z).toReal ≤ 1

    The real-valued conditional masses on a finite set S of distinct strings sum to at most 1. Pushes the ℝ≥0∞ fact condQkState_sum_le_one through .toReal (each term ≤ 1 < ⊤).

    Used by

      Conditional (k-state, length) grouping bound #

      theorem

      InformationTheory.Shannon.condState_grouping_lengthProfile_counts

      source
      {α : Type u_1} {σ : Type u_3} [DecidableEq σ] (phrases : Finset (List α)) (keyf : List α → σ × ℕ) (hkey2 : ∀ (w : List α), (keyf w).2 = w.length) (ℓ : ℕ) :
      ∑ g ∈ Finset.image keyf phrases with g.2 = ℓ, {w ∈ phrases | keyf w = g}.card = {w ∈ phrases | w.length = ℓ}.card
      Used by
        theorem

        InformationTheory.Shannon.condState_grouping_perFiber_logsum

        source
        {α : Type u_1} {Ω : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (k : ℕ) (phrases : Finset (List α)) (st : List α → Fin k → α) (hpos : ∀ w ∈ phrases, 0 < (condQkState μ p k (st w) w.length (toFinVec w.length w)).toReal) :
        ∑ g ∈ Finset.image (fun (w : List α) => (st w, w.length)) phrases, ↑{w ∈ phrases | (st w, w.length) = g}.card * Real.log ↑{w ∈ phrases | (st w, w.length) = g}.card ≤ ∑ g ∈ Finset.image (fun (w : List α) => (st w, w.length)) phrases, ∑ w ∈ phrases with (st w, w.length) = g, -Real.log (condQkState μ p k (st w) w.length (toFinVec w.length w)).toReal
        Used by
          theorem

          InformationTheory.Shannon.condState_grouping_bound

          source
          {α : Type u_1} {Ω : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (k : ℕ) (phrases : Finset (List α)) (st : List α → Fin k → α) (hpos : ∀ w ∈ phrases, 0 < (condQkState μ p k (st w) w.length (toFinVec w.length w)).toReal) :
          ↑phrases.card * Real.log ↑phrases.card ≤ ∑ w ∈ phrases, -Real.log (condQkState μ p k (st w) w.length (toFinVec w.length w)).toReal + ↑phrases.card * Real.log ↑(Finset.image (fun (w : List α) => (st w, w.length)) phrases).card

          Conditional (k-state, length) grouped entropy bound for an abstract phrase set.

          Given a finite phrase set phrases : Finset (List α), a k-state assignment st : List α → (Fin k → α), and positivity of the per-phrase conditional mass,

          c · log c ≤ ∑_{w ∈ phrases} -log (condQkState μ p k (st w) |w| (toFinVec |w| w))
            + c · log D,

          where c = #phrases and D = #{(st w, |w|)} is the number of distinct (k-state, length) pairs. This is the conditional analogue of the dead marginal bound lz78PhraseStrings_mul_log_le_sum_neg_log_marginal_add_overhead, with the grouping index lifted from length to (k-state, length) and the marginal replaced by the markovFactor-derived conditional sub-distribution condQkState.

          Used by

            State-marginalization (a finer partition has higher entropy) #

            theorem

            InformationTheory.Shannon.state_marginalization_bound

            source
            {σ : Type u_3} [DecidableEq σ] (G : Finset (σ × ℕ)) (kk : σ × ℕ → ℕ) (nStates : ℕ) (hfiber_le : ∀ ℓ ∈ Finset.image Prod.snd G, {g ∈ G | g.2 = ℓ}.card ≤ nStates) :
            ∑ ℓ ∈ Finset.image Prod.snd G, ↑(∑ g ∈ G with g.2 = ℓ, kk g) * Real.log ↑(∑ g ∈ G with g.2 = ℓ, kk g) ≤ ∑ g ∈ G, ↑(kk g) * Real.log ↑(kk g) + ↑(∑ g ∈ G, kk g) * Real.log ↑nStates

            The state-marginalization grouping inequality (abstract Finset/Real).

            Fibering a pair-indexed count function kk : (σ × ℕ) → ℕ by the length coordinate, the length-marginal ∑·log sum is bounded by the full pair ∑·log sum plus an entropy correction (∑ kk)·log nStates, provided every length fiber has at most nStates distinct states:

            ∑_ℓ (c_ℓ · log c_ℓ) ≤ ∑_g (c_g · log c_g) + (∑_g c_g) · log nStates,

            where c_ℓ = ∑_{g.2 = ℓ} kk g and c_g = kk g. This is the discrete form of H(state | length) ≤ log nStates: a finer partition (by (state, length)) carries at most log nStates more entropy per phrase than the coarser length-only partition. Applying card_mul_log_le_sum_group_mul_log_add_card_log inside each length fiber and bounding the fiber's group count ≤ nStates.

            Used by

              Conditional grouping bound with mean-length overhead #

              theorem

              InformationTheory.Shannon.condState_grouping_bound_mean

              source
              {α : Type u_1} {Ω : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (k : ℕ) (phrases : Finset (List α)) (st : List α → Fin k → α) (hpos : ∀ w ∈ phrases, 0 < (condQkState μ p k (st w) w.length (toFinVec w.length w)).toReal) (hlen1 : ∀ w ∈ phrases, 1 ≤ w.length) (hne : phrases.Nonempty) :
              ↑phrases.card * Real.log ↑phrases.card ≤ ∑ w ∈ phrases, -Real.log (condQkState μ p k (st w) w.length (toFinVec w.length w)).toReal + (↑phrases.card * Real.log ((∑ w ∈ phrases, ↑w.length) / ↑phrases.card) + ↑phrases.card + ↑phrases.card * Real.log ↑(Fintype.card α ^ k))

              Conditional (k-state, length) grouped entropy bound with mean-length overhead, the o(n) form used for LZ78 achievability.

              This is the mean-length / empirical-entropy upgrade of condState_grouping_bound: the loose c · log D overhead (worst-case Θ(n)) is replaced by the manifestly o(n) empirical-entropy overhead c · log (N / c) + c + c · log #states, where N = ∑_{w ∈ phrases} |w| is the total parsed length and #states = (Fintype.card α)^k:

              c · log c ≤ ∑_{w ∈ phrases} -log (condQkState μ p k (st w) |w| (toFinVec |w| w))
            + (c · log (N / c) + c + c · log #states).

              Here c · log (N / c) is the mean-length term (o(n) since the mean length is ~ log n for the LZ78 parse) and c · log #states = c · k · log (card α) is o(n) for fixed k (since c = O(n / log n)). The proof composes empirical_entropy_le_log_mean (length empirical entropy ≤ c·log(mean)+c), state_marginalization_bound (state correction ≤ c·log #states), and the per-fiber log-sum step of condState_grouping_bound.

              Used by