Skip to content

InformationTheory.Shannon.MultipleAccess.IIDAmbient

Imports 5

i.i.d. ambient measure for the multiple access channel #

This file provides the i.i.d. ambient probability space for the two-user MAC achievability theorem, the MAC analogue of InformationTheory/Shannon/IIDProductInput/Basic.lean.

Construction #

Given two input distributions p₁ : Measure α₁, p₂ : Measure α₂ (independent, the product p₁ ⊗ p₂) and a MAC channel W : MACChannel α₁ α₂ β = Kernel (α₁ × α₂) β, the per-coordinate joint law is

macJointDistribution p₁ p₂ W := (jointDistribution (p₁.prod p₂) W).map prodAssoc

on α₁ × α₂ × β (the channel-coding joint (p₁ ⊗ p₂) ⊗ₘ W on (α₁ × α₂) × β, reshaped to the right-nested triple). The ambient space is Ω := ℕ → α₁ × α₂ × β with μ := Measure.infinitePi (fun _ : ℕ => macJointDistribution p₁ p₂ W), and the three coordinate projections

macX1s i ω := (ω i).1
macX2s i ω := (ω i).2.1
macYs i ω := (ω i).2.2

supply all the iIndepFun / IdentDistrib / positivity regularity hypotheses that the gateway atoms macJTS_indep_prob_le_X1/_X2/_both and the correct-pair AEP macJointlyTypicalSet_prob_tendsto_one demand.

Per-coordinate joint distribution #

noncomputable def

InformationTheory.Shannon.MAC.macJointDistribution

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] (p₁ : MeasureTheory.Measure α₁) (p₂ : MeasureTheory.Measure α₂) (W : MACChannel α₁ α₂ β) :

MeasureTheory.Measure (α₁ × α₂ × β)

The per-coordinate MAC joint law on α₁ × α₂ × β: the channel-coding joint (p₁ ⊗ p₂) ⊗ₘ W on (α₁ × α₂) × β reshaped to the right-nested triple.

Equations

InformationTheory.Shannon.MAC.macJointDistribution p₁ p₂ W = MeasureTheory.Measure.map (⇑MeasurableEquiv.prodAssoc) (InformationTheory.Shannon.ChannelCoding.jointDistribution (p₁.prod p₂) W)

Instances For

Used by

instance

InformationTheory.Shannon.MAC.macJointDistribution.instIsProbabilityMeasure

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] :

MeasureTheory.IsProbabilityMeasure (macJointDistribution p₁ p₂ W)

Used by

Ambient measure on `ℕ → α₁ × α₂ × β` #

noncomputable def

InformationTheory.Shannon.MAC.macAmbientMeasure

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] (p₁ : MeasureTheory.Measure α₁) (p₂ : MeasureTheory.Measure α₂) (W : MACChannel α₁ α₂ β) :

MeasureTheory.Measure (ℕ → α₁ × α₂ × β)

The i.i.d. MAC ambient measure: Measure.infinitePi (fun _ => macJointDistribution p₁ p₂ W).

Equations

InformationTheory.Shannon.MAC.macAmbientMeasure p₁ p₂ W = MeasureTheory.Measure.infinitePi fun (x : ℕ) => InformationTheory.Shannon.MAC.macJointDistribution p₁ p₂ W

Instances For

Used by

instance

InformationTheory.Shannon.MAC.macAmbientMeasure.instIsProbabilityMeasure

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] :

MeasureTheory.IsProbabilityMeasure (macAmbientMeasure p₁ p₂ W)

Used by

def

InformationTheory.Shannon.MAC.macX1s

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} :

ℕ → (ℕ → α₁ × α₂ × β) → α₁

The first input coordinate ω ↦ (ω i).1.

Equations

InformationTheory.Shannon.MAC.macX1s i ω = (ω i).1

Instances For

Used by

def

InformationTheory.Shannon.MAC.macX2s

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} :

ℕ → (ℕ → α₁ × α₂ × β) → α₂

The second input coordinate ω ↦ (ω i).2.1.

Equations

InformationTheory.Shannon.MAC.macX2s i ω = (ω i).2.1

Instances For

Used by

def

InformationTheory.Shannon.MAC.macYs

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} :

ℕ → (ℕ → α₁ × α₂ × β) → β

The output coordinate ω ↦ (ω i).2.2.

Equations

InformationTheory.Shannon.MAC.macYs i ω = (ω i).2.2

Instances For

Used by

theorem

InformationTheory.Shannon.MAC.macX1s_apply

@[simp]

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (i : ℕ) (ω : ℕ → α₁ × α₂ × β) :

macX1s i ω = (ω i).1

Used by

theorem

InformationTheory.Shannon.MAC.macX2s_apply

@[simp]

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (i : ℕ) (ω : ℕ → α₁ × α₂ × β) :

macX2s i ω = (ω i).2.1

Used by

theorem

InformationTheory.Shannon.MAC.macYs_apply

@[simp]

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (i : ℕ) (ω : ℕ → α₁ × α₂ × β) :

macYs i ω = (ω i).2.2

Used by

theorem

InformationTheory.Shannon.MAC.measurable_macX1s

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] (i : ℕ) :

Measurable (macX1s i)

Used by

theorem

InformationTheory.Shannon.MAC.measurable_macX2s

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] (i : ℕ) :

Measurable (macX2s i)

Used by

theorem

InformationTheory.Shannon.MAC.measurable_macYs

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] (i : ℕ) :

Measurable (macYs i)

Used by

Generic coordinate-selector map / independence / positivity #

Every random variable consumed by the gateway atoms and the AEP has the form fun ω ↦ g (ω i) for a measurable coordinate selector g : α₁ × α₂ × β → γ.

theorem

InformationTheory.Shannon.MAC.macAmbient_map_coord

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] {γ : Type u_4} [MeasurableSpace γ] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] (g : α₁ × α₂ × β → γ) (hg : Measurable g) (i : ℕ) :

MeasureTheory.Measure.map (fun (ω : ℕ → α₁ × α₂ × β) => g (ω i)) (macAmbientMeasure p₁ p₂ W) = MeasureTheory.Measure.map g (macJointDistribution p₁ p₂ W)

The map of a coordinate selector under the ambient measure equals the map of the selector under the per-coordinate joint law.

Used by

theorem

InformationTheory.Shannon.MAC.macAmbient_iIndepFun_coord

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] {γ : Type u_4} [MeasurableSpace γ] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] (g : α₁ × α₂ × β → γ) (hg : Measurable g) :

ProbabilityTheory.iIndepFun (fun (i : ℕ) (ω : ℕ → α₁ × α₂ × β) => g (ω i)) (macAmbientMeasure p₁ p₂ W)

Mutual independence of any coordinate selector under the ambient measure.

Used by

theorem

InformationTheory.Shannon.MAC.macAmbient_pairwise_coord

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] {γ : Type u_4} [MeasurableSpace γ] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] (g : α₁ × α₂ × β → γ) (hg : Measurable g) :

Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (fun (ω : ℕ → α₁ × α₂ × β) => g (ω i)) (fun (ω : ℕ → α₁ × α₂ × β) => g (ω j)) (macAmbientMeasure p₁ p₂ W)

Pairwise independence of any coordinate selector.

Used by

theorem

InformationTheory.Shannon.MAC.macAmbient_identDistrib_coord

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] {γ : Type u_4} [MeasurableSpace γ] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] (g : α₁ × α₂ × β → γ) (hg : Measurable g) (i : ℕ) :

ProbabilityTheory.IdentDistrib (fun (ω : ℕ → α₁ × α₂ × β) => g (ω i)) (fun (ω : ℕ → α₁ × α₂ × β) => g (ω 0)) (macAmbientMeasure p₁ p₂ W) (macAmbientMeasure p₁ p₂ W)

Identical distribution of a coordinate selector across indices.

Used by

theorem

InformationTheory.Shannon.MAC.macAmbient_entropy_coord

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] {γ : Type u_4} [Fintype γ] [Nonempty γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] (g : α₁ × α₂ × β → γ) (hg : Measurable g) (i : ℕ) :

(entropy (macAmbientMeasure p₁ p₂ W) fun (ω : ℕ → α₁ × α₂ × β) => g (ω i)) = entropy (macJointDistribution p₁ p₂ W) g

Entropy of a coordinate selector under the ambient measure equals its entropy under the per-coordinate joint law.

Used by

Positivity of the per-coordinate joint law and coordinate marginals #

theorem

InformationTheory.Shannon.MAC.prod_real_singleton_pos

{α₁ : Type u_1} {α₂ : Type u_2} [MeasurableSpace α₁] [MeasurableSpace α₂] [Fintype α₂] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (hp₁ : ∀ (a : α₁), 0 < p₁.real {a}) (hp₂ : ∀ (a : α₂), 0 < p₂.real {a}) (q : α₁ × α₂) :

0 < (p₁.prod p₂).real {q}

The product input law has positive singleton mass.

Used by

theorem

InformationTheory.Shannon.MAC.macJointDistribution_real_singleton_pos

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] [Fintype α₁] [MeasurableSingletonClass α₁] [Fintype α₂] [MeasurableSingletonClass α₂] [MeasurableSingletonClass β] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] (hp₁ : ∀ (a : α₁), 0 < p₁.real {a}) (hp₂ : ∀ (a : α₂), 0 < p₂.real {a}) (hW : ∀ (a : α₁ × α₂) (b : β), 0 < (W a).real {b}) (q : α₁ × α₂ × β) :

0 < (macJointDistribution p₁ p₂ W).real {q}

The per-coordinate MAC joint law has positive singleton mass.

Used by

theorem

InformationTheory.Shannon.MAC.macAmbient_map_coord_real_singleton_pos

{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [MeasurableSpace α₁] [MeasurableSpace α₂] [MeasurableSpace β] [Fintype α₁] [MeasurableSingletonClass α₁] [Fintype α₂] [MeasurableSingletonClass α₂] [MeasurableSingletonClass β] {γ : Type u_4} [MeasurableSpace γ] [MeasurableSingletonClass γ] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] (hp₁ : ∀ (a : α₁), 0 < p₁.real {a}) (hp₂ : ∀ (a : α₂), 0 < p₂.real {a}) (hW : ∀ (a : α₁ × α₂) (b : β), 0 < (W a).real {b}) (g : α₁ × α₂ × β → γ) (hg : Measurable g) (i : ℕ) (q : γ) (r : α₁ × α₂ × β) (hr : g r = q) :

0 < (MeasureTheory.Measure.map (fun (ω : ℕ → α₁ × α₂ × β) => g (ω i)) (macAmbientMeasure p₁ p₂ W)).real {q}

Positivity of any coordinate-selector marginal singleton, reduced to the per-coordinate joint positivity via a chosen fiber witness.

Used by