InformationTheory.Shannon.SlepianWolf.ConditionalTypicalSlice
Slepian–Wolf conditional typical slice #
This file publishes the conditional typical slice size bound, the key new
ingredient for the full Slepian–Wolf rate region (Cover–Thomas).
For a fixed Y-block y : Fin n → β, the X-fiber of the jointly typical set
is bounded in size by exp(n · (H(X|Y) + 2ε)), where H(X|Y) := H(X, Y) - H(Y).
Main definitions #
conditionalTypicalSlice μ Xs Ys n ε y— the fiber{x : Fin n → α | (x, y) ∈ jointlyTypicalSet μ Xs Ys n ε}.
Main statements #
conditionalTypicalSlice_card_le— the slice size is bounded byexp(n · (H(X, Y) - H(Y) + 2ε)).
Implementation notes #
- Each fiber element
xmakes(x, y)jointly typical, so the joint sequencei ↦ (x i, y i)lies intypicalSet μ (jointSequence Xs Ys) n εand each sample has probability at leastexp(-n · (H(X, Y) + ε))bytypicalSet_prob_ge. Summed over the fiber this is at mostPr[Yⁿ = y], which forY-typicalyis at mostexp(-n · (H(Y) - ε))bytypicalSet_prob_le.
Definition of the conditional typical slice #
InformationTheory.Shannon.ChannelCoding.conditionalTypicalSlice
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[MeasurableSpace α]
{β : Type u_3}
[Fintype β]
[MeasurableSpace β]
(μ : MeasureTheory.Measure Ω)
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
(n : ℕ)
(ε : ℝ)
(y : Fin n → β)
:
The conditional typical slice at y: the X-fiber of the jointly
typical set jointlyTypicalSet μ Xs Ys n ε at the Y-block y. Each
element x of this slice forms a jointly typical pair (x, y).
Equations
Instances For
Used by
InformationTheory.Shannon.ChannelCoding.mem_conditionalTypicalSlice_iff
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[MeasurableSpace α]
{β : Type u_3}
[Fintype β]
[MeasurableSpace β]
(μ : MeasureTheory.Measure Ω)
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
(n : ℕ)
(ε : ℝ)
(y : Fin n → β)
(x : Fin n → α)
:
Used by
InformationTheory.Shannon.ChannelCoding.conditionalTypicalSlice_finite
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
{β : Type u_3}
[Fintype β]
[Nonempty β]
[MeasurableSpace β]
[MeasurableSingletonClass β]
(μ : MeasureTheory.Measure Ω)
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
(n : ℕ)
(ε : ℝ)
(y : Fin n → β)
:
(conditionalTypicalSlice μ Xs Ys n ε y).Finite
The slice is finite (it lives in the finite ambient space Fin n → α).
Used by
InformationTheory.Shannon.ChannelCoding.conditionalTypicalSlice_empty_of_y_not_typical
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[MeasurableSpace α]
{β : Type u_3}
[Fintype β]
[MeasurableSpace β]
(μ : MeasureTheory.Measure Ω)
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
(n : ℕ)
(ε : ℝ)
{y : Fin n → β}
(hy : y ∉ typicalSet μ Ys n ε)
:
The slice is empty when y is not Y-typical.
Used by
Main bound — fiber cardinality #
InformationTheory.Shannon.ChannelCoding.conditionalTypicalSlice_card_le
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))
(hindepY_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Ys i) μ)
(hidentY : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Ys i) (Ys 0) μ μ)
(hindepZ_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => jointSequence Xs Ys i) μ)
(hidentZ : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (jointSequence Xs Ys i) (jointSequence Xs Ys 0) μ μ)
(hposY : ∀ (y : β), 0 < (MeasureTheory.Measure.map (Ys 0) μ).real {y})
(hposZ : ∀ (p : α × β), 0 < (MeasureTheory.Measure.map (jointSequence Xs Ys 0) μ).real {p})
(n : ℕ)
{ε : ℝ}
(y : Fin n → β)
:
Conditional typical slice size bound: for any Y-block y, the
cardinality of the X-fiber of the jointly typical set at y is at most
exp(n · (H(X, Y) - H(Y) + 2ε)), equivalently exp(n · (H(X|Y) + 2ε)).