InformationTheory.Shannon.MultipleAccess.Basic

Imports 3

Multiple access channel — primitive definitions #

Two-user multiple access channel (MAC) primitives, following the single-user InformationTheory.Shannon.ChannelCoding.Basic conventions (Cover–Thomas).

Main definitions #

MACChannel α₁ α₂ β := Kernel (α₁ × α₂) β — a discrete MAC with two inputs and one output.
MACCode M₁ M₂ n α₁ α₂ β — a two-user block code: two encoders and a joint pair decoder.
MACCode.errorProbAt / MACCode.averageErrorProb — the pointwise and uniform-average block-decoding error probabilities.
InMACCapacityRegion R₁ R₂ I₁ I₂ Iboth — the corner-point capacity-region predicate: R₁ ≤ I₁, R₂ ≤ I₂, R₁ + R₂ ≤ Iboth.

abbrev

InformationTheory.Shannon.MAC.MACChannel

source

@[reducible, inline]

(α₁ : Type u_4) (α₂ : Type u_5) (β : Type u_6) [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] :

Type (max (max u_5 u_4) u_6)

A discrete memoryless multiple access channel: a Markov kernel from the joint input α₁ × α₂ to the output β.

Equations

InformationTheory.Shannon.MAC.MACChannel α₁ α₂ β = ProbabilityTheory.Kernel (α₁ × α₂) β

Instances For

Used by

structure

InformationTheory.Shannon.MAC.MACCode

source

(M₁ M₂ n : ℕ) (α₁ : Type u_4) (α₂ : Type u_5) (β : Type u_6) [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] :

Type (max (max u_4 u_5) u_6)

A two-user MAC block code of length n: an encoder for each user and a joint pair decoder. As in the single-user Code, no measurability fields are bundled (all functions on finite alphabets are automatically measurable).

encoder₁ : Fin M₁ → Fin n → α₁
Encoder for user 1.
encoder₂ : Fin M₂ → Fin n → α₂
Encoder for user 2.
decoder : (Fin n → β) → Fin M₁ × Fin M₂
Joint pair decoder.

Instances For

Used by

def

InformationTheory.Shannon.MAC.MACCode.decodingRegion

source

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] {M₁ M₂ n : ℕ} (c : MACCode M₁ M₂ n α₁ α₂ β) (m : Fin M₁ × Fin M₂) :

Set (Fin n → β)

Decoding region for the message pair m: outputs y decoded as m.

Equations

c.decodingRegion m = {y : Fin n → β | c.decoder y = m}

Instances For

Used by

def

InformationTheory.Shannon.MAC.MACCode.errorEvent

source

Set (Fin n → β)

The joint error event for the pair m: outputs decoded as anything other than m. A single event captures all three MAC error types (user 1 wrong, user 2 wrong, both wrong).

Equations

c.errorEvent m = (c.decodingRegion m)ᶜ

Instances For

Used by

theorem

InformationTheory.Shannon.MAC.MACCode.mem_errorEvent

source

@[simp]

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] {M₁ M₂ n : ℕ} (c : MACCode M₁ M₂ n α₁ α₂ β) (m : Fin M₁ × Fin M₂) (y : Fin n → β) :

y ∈ c.errorEvent m ↔ c.decoder y ≠ m

Used by

noncomputable def

InformationTheory.Shannon.MAC.MACCode.errorProbAt

source

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] {M₁ M₂ n : ℕ} (c : MACCode M₁ M₂ n α₁ α₂ β) (W : MACChannel α₁ α₂ β) (m : Fin M₁ × Fin M₂) :

ENNReal

Pointwise error probability when the pair m = (m₁, m₂) is sent: the memoryless block output law is Measure.pi (i ↦ W (encoder₁ m₁ i, encoder₂ m₂ i)).

Equations

c.errorProbAt W m = (MeasureTheory.Measure.pi fun (i : Fin n) => W (c.encoder₁ m.1 i, c.encoder₂ m.2 i)) (c.errorEvent m)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.MAC.MACCode.averageErrorProb

source

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] {M₁ M₂ n : ℕ} (c : MACCode M₁ M₂ n α₁ α₂ β) (W : MACChannel α₁ α₂ β) :

ENNReal

Average error probability under a uniform message pair: (1/(M₁·M₂)) ∑ m, errorProbAt. For M₁·M₂ = 0 we set this to 0.

Equations

c.averageErrorProb W = if M₁ * M₂ = 0 then 0 else (↑(M₁ * M₂))⁻¹ * ∑ m : Fin M₁ × Fin M₂, c.errorProbAt W m

Instances For

Used by

theorem

InformationTheory.Shannon.MAC.MACCode.errorProbAt_le_one

source

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] {M₁ M₂ n : ℕ} (c : MACCode M₁ M₂ n α₁ α₂ β) (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] (m : Fin M₁ × Fin M₂) :

c.errorProbAt W m ≤ 1

Each pointwise error probability is at most 1 (the block output law is a probability measure for a Markov kernel).

Used by

theorem

InformationTheory.Shannon.MAC.MACCode.averageErrorProb_le_one

source

c.averageErrorProb W ≤ 1

The average error probability is at most 1.

Used by

theorem

InformationTheory.Shannon.MAC.MACCode.averageErrorProb_ne_top

source

c.averageErrorProb W ≠ ⊤

The average error probability is finite.

Used by

Corner-point capacity region #

structure

InformationTheory.Shannon.MAC.InMACCapacityRegion

source

(R₁ R₂ I₁ I₂ Iboth : ℝ) :

Prop

The corner-point capacity-region predicate: a generic bundle of the three inequalities R₁ ≤ I₁, R₂ ≤ I₂, R₁ + R₂ ≤ Iboth on five real numbers. The slots I₁, I₂, Iboth are abstract information bounds — the predicate does not fix their meaning. Two distinct instantiations are intended:

message level (proven, mac_converse_message_level): I₁, I₂, Iboth are the n-letter message–output mutual informations plus Fano terms.
single letter (not yet done — the standard Cover–Thomas form): after single-letterization, I₁ = I(X₁; Y | X₂), I₂ = I(X₂; Y | X₁), Iboth = I(X₁, X₂; Y).

InMACCapacityRegion.mono (enlarging the information bounds keeps the rate pair inside) is the bridge from the message-level form to the single-letter form.

bound₁ : R₁ ≤ I₁
User-1 rate bound.
bound₂ : R₂ ≤ I₂
User-2 rate bound.
boundSum : R₁ + R₂ ≤ Iboth
Sum-rate bound.

Instances For

Used by

theorem

InformationTheory.Shannon.MAC.InMACCapacityRegion.mono

source

{R₁ R₂ I₁ I₂ Iboth I₁' I₂' Iboth' : ℝ} (h : InMACCapacityRegion R₁ R₂ I₁ I₂ Iboth) (h₁ : I₁ ≤ I₁') (h₂ : I₂ ≤ I₂') (hsum : Iboth ≤ Iboth') :

InMACCapacityRegion R₁ R₂ I₁' I₂' Iboth'

Monotonicity of the region in the information bounds: enlarging I₁, I₂, Iboth keeps the rate pair inside.

Used by