InformationTheory

InformationTheory.Shannon.SlepianWolf.Binning

source

Imports 5

Slepian–Wolf random binning machinery #

This file introduces the random-binning measure binningMeasure α n M on the hash-function space (Fin n → α) → Fin M, plus the collision-probability collapse 𝔼_f[1_{f x = f x'}] = 1/M for x ≠ x' (and = 1 for x = x').

Main definitions #

  • binningMeasure α n M — Measure.pi (fun _ : (Fin n → α) => uniformOn univ) on (Fin n → α) → Fin M.

Main statements #

Implementation notes #

  • This is the encoder-side mirror of ChannelCodingAchievability.codebookMeasure (Measure.pi (fun _ : Fin M => Measure.pi (fun _ : Fin n => p))): the index of the outer Measure.pi is swapped from Fin M (codeword count) to (Fin n → α) (input-sequence space).

References #

  • T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.

The random binning measure and basic instances #

noncomputable def

InformationTheory.Shannon.binningMeasure

source
(α : Type u_2) [Fintype α] [MeasurableSpace α] (n M : ℕ) [NeZero M] :
MeasureTheory.Measure ((Fin n → α) → Fin M)

Random binning measure. Each input sequence x ∈ (Fin n → α) is hashed independently to a uniformly random bin index in Fin M. The total law on the hash-function space (Fin n → α) → Fin M is the product of |α|^n copies of uniformOn (Set.univ : Set (Fin M)).

Encoder-side mirror of ChannelCodingAchievability.codebookMeasure:

  • codebookMeasure p M n = Measure.pi (fun _ : Fin M => Measure.pi (fun _ : Fin n => p)) ("Fin M codewords drawn i.i.d. from p^n").
  • binningMeasure α n M = Measure.pi (fun _ : (Fin n → α) => uniformOn univ) ("|α|^n hash bins drawn uniformly").

The outer-Measure.pi index is the input-sequence space (Fin n → α), which is a Fintype because α is finite.

Equations
Instances For
    Used by
      instance

      InformationTheory.Shannon.binningMeasure.instIsProbabilityMeasure

      source
      {α : Type u_1} [Fintype α] [MeasurableSpace α] (n M : ℕ) [NeZero M] :
      MeasureTheory.IsProbabilityMeasure (binningMeasure α n M)

      The random binning measure is a probability measure.

      Used by
        theorem

        InformationTheory.Shannon.binningMeasure_singleton_real

        source
        {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (n M : ℕ) [NeZero M] (f : (Fin n → α) → Fin M) :
        (binningMeasure α n M).real {f} = (↑M)⁻¹ ^ Fintype.card (Fin n → α)

        Singleton mass. For any hash function f : (Fin n → α) → Fin M, its binningMeasure-mass is (1/M)^{|α|^n} (each of the |α|^n input sequences independently picks one of M bins).

        Used by

          Collision probability collapse 𝔼[1_{f x = f x'}] = 1/M #

          theorem

          InformationTheory.Shannon.binning_collision_prob

          source
          {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {n M : ℕ} [NeZero M] {x x' : Fin n → α} (h : x ≠ x') :
          (binningMeasure α n M).real {f : (Fin n → α) → Fin M | f x = f x'} = (↑M)⁻¹

          For random binning at rate 1/M per input sequence, two distinct sequences x ≠ x' collide with probability exactly 1/M.

          Used by