InformationTheory.Shannon.SlepianWolf.FullRateRegion.Core

noncomputable def

InformationTheory.Shannon.ChannelCoding.swJointTypicalDecoder

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] {β : Type u_3} [Fintype β] [Nonempty β] [MeasurableSpace β] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) {n M_X M_Y : ℕ} (ε : ℝ) (f_X : (Fin n → α) → Fin M_X) (f_Y : (Fin n → β) → Fin M_Y) :

Fin M_X × Fin M_Y → (Fin n → α) × (Fin n → β)

Slepian–Wolf joint typicality decoder. Given a bin pair (i, j), returns the unique source pair (x, y) consistent with the bins whose joint sequence is jointly typical, falling back to an arbitrary source pair if either no such pair exists or it is not unique.

Equations

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

Instances For

Used by

def

InformationTheory.Shannon.ChannelCoding.swError_E0

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] {β : Type u_3} [Fintype β] [MeasurableSpace β] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) (n : ℕ) (ε : ℝ) :

Set Ω

E_0: the true source pair is not jointly typical.

Equations

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

Instances For

Used by

def

InformationTheory.Shannon.ChannelCoding.swError_EX

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] {β : Type u_3} [Fintype β] [MeasurableSpace β] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) (n : ℕ) {M_X : ℕ} (ε : ℝ) (f_X : (Fin n → α) → Fin M_X) :

Set Ω

E_X: there exists an alias x' ≠ X^n colliding with X^n under f_X such that (x', Y^n) is jointly typical.

Equations

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

Instances For

Used by

def

InformationTheory.Shannon.ChannelCoding.swError_EY

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] {β : Type u_3} [Fintype β] [MeasurableSpace β] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) (n : ℕ) {M_Y : ℕ} (ε : ℝ) (f_Y : (Fin n → β) → Fin M_Y) :

Set Ω

E_Y: there exists an alias y' ≠ Y^n colliding with Y^n under f_Y such that (X^n, y') is jointly typical.

Equations

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

Instances For

Used by

def

InformationTheory.Shannon.ChannelCoding.swError_EXY

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] {β : Type u_3} [Fintype β] [MeasurableSpace β] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) (n : ℕ) {M_X M_Y : ℕ} (ε : ℝ) (f_X : (Fin n → α) → Fin M_X) (f_Y : (Fin n → β) → Fin M_Y) :

Set Ω

E_{XY}: there exists an alias pair p ≠ (X^n, Y^n) colliding with (X^n, Y^n) under (f_X, f_Y) on both axes such that p is jointly typical.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.ChannelCoding.swJointTypicalDecoder_eq_of_unique

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {β : Type u_3} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) {n M_X M_Y : ℕ} (ε : ℝ) (f_X : (Fin n → α) → Fin M_X) (f_Y : (Fin n → β) → Fin M_Y) {ω : Ω} (htrue : (jointRV Xs n ω, jointRV Ys n ω) ∈ jointlyTypicalSet μ Xs Ys n ε) (hunique : ∀ (p : (Fin n → α) × (Fin n → β)), f_X p.1 = f_X (jointRV Xs n ω) → f_Y p.2 = f_Y (jointRV Ys n ω) → p ∈ jointlyTypicalSet μ Xs Ys n ε → p = (jointRV Xs n ω, jointRV Ys n ω)) :

swJointTypicalDecoder μ Xs Ys ε f_X f_Y (f_X (jointRV Xs n ω), f_Y (jointRV Ys n ω)) = (jointRV Xs n ω, jointRV Ys n ω)

If (X^n, Y^n) is jointly typical and is the unique source pair (across all source pairs) compatible with its bin pair under joint typicality, then the joint typical decoder recovers it exactly.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.swErrorProb_le_E0_plus_EX_plus_EY_plus_EXY

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {β : Type u_3} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hYs : ∀ (i : ℕ), Measurable (Ys i)) {n M_X M_Y : ℕ} (ε : ℝ) (f_X : (Fin n → α) → Fin M_X) (f_Y : (Fin n → β) → Fin M_Y) :

swErrorProb μ (jointRV Xs n) (jointRV Ys n) f_X f_Y (swJointTypicalDecoder μ Xs Ys ε f_X f_Y) ≤ μ.real (swError_E0 μ Xs Ys n ε) + μ.real (swError_EX μ Xs Ys n ε f_X) + μ.real (swError_EY μ Xs Ys n ε f_Y) + μ.real (swError_EXY μ Xs Ys n ε f_X f_Y)

Main 4-way error decomposition. The Slepian–Wolf error probability under the joint typicality decoder is bounded above by the sum of probabilities of the four error events E_0, E_X, E_Y, E_{XY}.

hXs / hYs are kept in the signature as part of the public API (downstream random-binning average bounds need them) even though this pointwise subset argument does not consume them.

Used by

theorem