InformationTheory.Shannon.MultipleAccess.JointTypicality

Imports 3

Multiple access channel — three-way jointly typical set #

The three-way jointly typical set for a two-user MAC, following the single-user InformationTheory.Shannon.ChannelCoding.jointlyTypicalSet conventions (Cover–Thomas).

Design #

The single-user typical set InformationTheory.Shannon.typicalSet is an entropy-typicality set (empirical entropy within ε of the true entropy), not a strong / letter-typicality set. Consequently a three-way (X₁, X₂, Y)-joint-typical triple does not by itself entail any of the pairwise-typical facts (e.g. (X₂, Y)-pair-typical). The achievability error analysis needs those pairwise facts to bound the conditional-fibre masses, so macJointlyTypicalSet is defined as the intersection of all the single-axis, pairwise, and three-way typicality conditions.

This shape makes each of the three "one user uses a wrong codeword" reductions a syntactic instance of the single-user jointly-typical set under regrouping:

user 1 wrong: X₁ ⟂ (X₂, Y) reduces to jointlyTypicalSet μ X₁s (jointSequence X₂s Ys),
user 2 wrong: X₂ ⟂ (X₁, Y) reduces to jointlyTypicalSet μ X₂s (jointSequence X₁s Ys),
both wrong: (X₁, X₂) ⟂ Y reduces to jointlyTypicalSet μ (jointSequence X₁s X₂s) Ys.

Main definitions #

macJointSequence X₁s X₂s Ys — the three-way joint sequence i ω ↦ (X₁s i ω, X₂s i ω, Ys i ω).
macJointlyTypicalSet μ X₁s X₂s Ys n ε — the three-way jointly typical set, the intersection of the three single-axis, three pairwise, and one three-way typicality conditions.

noncomputable def

InformationTheory.Shannon.MAC.macJointSequence

source

{Ω : Type u_1} {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} (X1s : ℕ → Ω → α₁) (X2s : ℕ → Ω → α₂) (Ys : ℕ → Ω → β) :

ℕ → Ω → α₁ × α₂ × β

The three-way joint sequence over the product alphabet α₁ × α₂ × β. Definitionally equal to jointSequence X₁s (jointSequence X₂s Ys) (right-associated nesting).

Equations

InformationTheory.Shannon.MAC.macJointSequence X1s X2s Ys i ω = (X1s i ω, X2s i ω, Ys i ω)

Instances For

Used by

theorem

InformationTheory.Shannon.MAC.macJointSequence_eq

source

{Ω : Type u_1} {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} (X1s : ℕ → Ω → α₁) (X2s : ℕ → Ω → α₂) (Ys : ℕ → Ω → β) :

macJointSequence X1s X2s Ys = ChannelCoding.jointSequence X1s (ChannelCoding.jointSequence X2s Ys)

Used by

theorem

InformationTheory.Shannon.MAC.measurable_macJointSequence

source

{Ω : Type u_1} [MeasurableSpace Ω] {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] (X1s : ℕ → Ω → α₁) (X2s : ℕ → Ω → α₂) (Ys : ℕ → Ω → β) (hX1s : ∀ (i : ℕ), Measurable (X1s i)) (hX2s : ∀ (i : ℕ), Measurable (X2s i)) (hYs : ∀ (i : ℕ), Measurable (Ys i)) (i : ℕ) :

Measurable (macJointSequence X1s X2s Ys i)

Used by

noncomputable def

InformationTheory.Shannon.MAC.macJointlyTypicalSet

source

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

Set ((Fin n → α₁) × (Fin n → α₂) × (Fin n → β))

The three-way jointly typical set A_ε^n ⊆ (Fin n → α₁) × (Fin n → α₂) × (Fin n → β): triples (x₁, x₂, y) that are simultaneously typical along every single axis, every pair of axes, and the three-way joint axis. The seven conditions are exactly what the three achievability error events E1/E2/E3 require.

@audit:ok

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.MAC.mem_macJointlyTypicalSet_iff

source

(x1, x2, y) ∈ macJointlyTypicalSet μ X1s X2s Ys n ε ↔ x1 ∈ typicalSet μ X1s n ε ∧ x2 ∈ typicalSet μ X2s n ε ∧ y ∈ typicalSet μ Ys n ε ∧ (fun (i : Fin n) => (x1 i, x2 i)) ∈ typicalSet μ (ChannelCoding.jointSequence X1s X2s) n ε ∧ (fun (i : Fin n) => (x1 i, y i)) ∈ typicalSet μ (ChannelCoding.jointSequence X1s Ys) n ε ∧ (fun (i : Fin n) => (x2 i, y i)) ∈ typicalSet μ (ChannelCoding.jointSequence X2s Ys) n ε ∧ (fun (i : Fin n) => (x1 i, x2 i, y i)) ∈ typicalSet μ (macJointSequence X1s X2s Ys) n ε

Used by

theorem

InformationTheory.Shannon.MAC.measurableSet_macJointlyTypicalSet

source

MeasurableSet (macJointlyTypicalSet μ X1s X2s Ys n ε)

Used by

theorem

InformationTheory.Shannon.MAC.macJointlyTypicalSet_finite

source

(macJointlyTypicalSet μ X1s X2s Ys n ε).Finite

Used by

theorem

InformationTheory.Shannon.MAC.macJointlyTypicalSet_prob_tendsto_one

source

Filter.Tendsto (fun (n : ℕ) => μ {ω : Ω | (jointRV X1s n ω, jointRV X2s n ω, jointRV Ys n ω) ∈ macJointlyTypicalSet μ X1s X2s Ys n ε}) Filter.atTop (nhds 1)

Bound (a): three-way joint AEP probability. The probability that the correct codeword triple (X₁ⁿ, X₂ⁿ, Yⁿ) lies in the three-way jointly typical set tends to 1.

The seven typicality conditions (three single-axis, three pairwise, one three-way) each hold with probability tending to 1 by the single-sequence AEP (InformationTheory.Shannon.typicalSet_prob_tendsto_one); their intersection then tends to 1 by the complement-union bound. The independence / identical-distribution hypotheses are stated separately for each of the seven sub-sequences, matching the single-user jointlyTypicalSet_prob_tendsto_one template.

Used by