Skip to content

InformationTheory.Shannon.IIDProductInput.Basic

Imports 4

i.i.d. ambient `(μ, Xs, Ys)` for channel coding achievability #

This file provides the i.i.d. ambient probability space consumed by the abstract random_codebook_average_le and the main theorem channel_coding_achievability of InformationTheory/Shannon/ChannelCoding/Achievability.lean.

Construction #

Given an input distribution p : Measure α (a probability measure) and a channel W : Channel α β (a Markov kernel), the i.i.d. ambient space is Ω := ℕ → α × β equipped with the product measure μ := Measure.infinitePi (fun _ : ℕ => jointDistribution p W). Random variables are coordinate projections:

iidXs i ω := (ω i).1 — the i-th input symbol
iidYs i ω := (ω i).2 — the i-th output symbol

These exactly match the abstract Xs, Ys hypothesis shapes (iIndepFun, IdentDistrib, marginal-matching) demanded by the achievability lemmas.

Channel positivity #

The hposY / hposZ positivity lemmas require the channel-positivity hypothesis ∀ a y, 0 < W a {y} (in addition to input positivity ∀ a, 0 < p.real {a}). Without it outputDistribution p W and jointDistribution p W can hit zero on some singleton.

Ambient measure on `ℕ → α × β` #

noncomputable def

InformationTheory.Shannon.ChannelCoding.iidAmbientMeasure

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (p : MeasureTheory.Measure α) (W : Channel α β) :

MeasureTheory.Measure (ℕ → α × β)

The i.i.d. ambient measure for input distribution p and channel W: Measure.infinitePi (fun _ : ℕ => jointDistribution p W) on ℕ → α × β.

Equations

InformationTheory.Shannon.ChannelCoding.iidAmbientMeasure p W = MeasureTheory.Measure.infinitePi fun (x : ℕ) => InformationTheory.Shannon.ChannelCoding.jointDistribution p W

Instances For

Used by

instance

InformationTheory.Shannon.ChannelCoding.iidAmbientMeasure.instIsProbabilityMeasure

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

MeasureTheory.IsProbabilityMeasure (iidAmbientMeasure p W)

Used by

def

InformationTheory.Shannon.ChannelCoding.iidXs

{α : Type u_1} {β : Type u_2} :

ℕ → (ℕ → α × β) → α

The i-th input random variable: ω ↦ (ω i).1.

Equations

InformationTheory.Shannon.ChannelCoding.iidXs i ω = (ω i).1

Instances For

Used by

def

InformationTheory.Shannon.ChannelCoding.iidYs

{α : Type u_1} {β : Type u_2} :

ℕ → (ℕ → α × β) → β

The i-th output random variable: ω ↦ (ω i).2.

Equations

InformationTheory.Shannon.ChannelCoding.iidYs i ω = (ω i).2

Instances For

Used by

theorem

InformationTheory.Shannon.ChannelCoding.iidXs_apply

@[simp]

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

iidXs i ω = (ω i).1

Used by

theorem

InformationTheory.Shannon.ChannelCoding.iidYs_apply

@[simp]

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

iidYs i ω = (ω i).2

Used by

theorem

InformationTheory.Shannon.ChannelCoding.measurable_iidXs

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

Measurable (iidXs i)

Used by

theorem

InformationTheory.Shannon.ChannelCoding.measurable_iidYs

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

Measurable (iidYs i)

Used by

theorem

InformationTheory.Shannon.ChannelCoding.jointSequence_iidXs_iidYs

{α : Type u_1} {β : Type u_2} (i : ℕ) :

jointSequence iidXs iidYs i = fun (ω : ℕ → α × β) => ω i

The joint sequence collapses to the raw coordinate projection fun ω ↦ ω i modulo Prod.mk η.

Used by

Marginal laws #

The three coordinate-marginal identifications μ.map (Xs 0) = p, μ.map (Ys 0) = outputDistribution p W, μ.map (jointSequence Xs Ys 0) = jointDistribution p W.

theorem

InformationTheory.Shannon.ChannelCoding.iidAmbient_map_jointSequence

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (i : ℕ) :

MeasureTheory.Measure.map (jointSequence iidXs iidYs i) (iidAmbientMeasure p W) = jointDistribution p W

The joint sequence marginal at index i is the joint distribution p ⊗ₘ W.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.iidAmbient_map_iidXs

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (i : ℕ) :

MeasureTheory.Measure.map (iidXs i) (iidAmbientMeasure p W) = p

The input marginal μ.map (Xs i) = p.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.iidAmbient_map_iidYs

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (i : ℕ) :

MeasureTheory.Measure.map (iidYs i) (iidAmbientMeasure p W) = outputDistribution p W

The output marginal μ.map (Ys i) = outputDistribution p W.

Used by

`IdentDistrib` along each axis #

theorem

InformationTheory.Shannon.ChannelCoding.iidAmbient_identDistrib_iidXs

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (i : ℕ) :

ProbabilityTheory.IdentDistrib (iidXs i) (iidXs 0) (iidAmbientMeasure p W) (iidAmbientMeasure p W)

Used by

theorem

InformationTheory.Shannon.ChannelCoding.iidAmbient_identDistrib_iidYs

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (i : ℕ) :

ProbabilityTheory.IdentDistrib (iidYs i) (iidYs 0) (iidAmbientMeasure p W) (iidAmbientMeasure p W)

Used by

theorem

InformationTheory.Shannon.ChannelCoding.iidAmbient_identDistrib_joint

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (i : ℕ) :

ProbabilityTheory.IdentDistrib (jointSequence iidXs iidYs i) (jointSequence iidXs iidYs 0) (iidAmbientMeasure p W) (iidAmbientMeasure p W)

Used by

`iIndepFun` along each axis #

theorem

InformationTheory.Shannon.ChannelCoding.iidAmbient_iIndepFun_iidXs

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

ProbabilityTheory.iIndepFun (fun (i : ℕ) => iidXs i) (iidAmbientMeasure p W)

The input coordinates Xs i ω = (ω i).1 are mutually independent under the i.i.d. ambient measure.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.iidAmbient_iIndepFun_iidYs

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

ProbabilityTheory.iIndepFun (fun (i : ℕ) => iidYs i) (iidAmbientMeasure p W)

The output coordinates Ys i ω = (ω i).2 are mutually independent.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.iidAmbient_iIndepFun_joint

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

ProbabilityTheory.iIndepFun (fun (i : ℕ) => jointSequence iidXs iidYs i) (iidAmbientMeasure p W)

The joint coordinate sequence jointSequence iidXs iidYs i ω = ω i is mutually independent.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.iidAmbient_pairwise_indep_joint

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

Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (jointSequence iidXs iidYs i) (jointSequence iidXs iidYs j) (iidAmbientMeasure p W)

Pairwise independence for the joint axis: needed by jointlyTypicalSet_prob_tendsto_one (which takes the Pairwise … ⟂ᵢ[μ] … form rather than the full iIndepFun form).

Used by

theorem

InformationTheory.Shannon.ChannelCoding.iidAmbient_pairwise_indep_iidXs

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

Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (iidXs i) (iidXs j) (iidAmbientMeasure p W)

Used by

theorem

InformationTheory.Shannon.ChannelCoding.iidAmbient_pairwise_indep_iidYs

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

Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (iidYs i) (iidYs j) (iidAmbientMeasure p W)

Used by

Positivity of singleton marginals #

theorem

InformationTheory.Shannon.ChannelCoding.jointDistribution_singleton

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (x : α) (y : β) :

(jointDistribution p W) {(x, y)} = p {x} * (W x) {y}

Singleton mass of the joint distribution: (p ⊗ₘ W) {(x, y)} = p {x} * W x {y}. Uses Set.singleton_prod_singleton to rewrite the singleton as a product set and then compProd_apply_prod + lintegral_singleton to evaluate.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.jointDistribution_singleton_pos

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (hp_pos : ∀ (a : α), 0 < p.real {a}) (hW_pos : ∀ (a : α) (b : β), 0 < (W a).real {b}) (x : α) (y : β) :

0 < (jointDistribution p W).real {(x, y)}

Positivity of (jointDistribution p W).real {(x, y)} from input + channel positivity.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.iidAmbient_iidXs_real_singleton_pos

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (hp_pos : ∀ (a : α), 0 < p.real {a}) (x : α) :

0 < (MeasureTheory.Measure.map (iidXs 0) (iidAmbientMeasure p W)).real {x}

Positivity of the input marginal: 0 < (μ.map (iidXs 0)).real {x}.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.iidAmbient_iidYs_real_singleton_pos

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [MeasurableSingletonClass β] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (hp_pos : ∀ (a : α), 0 < p.real {a}) (hW_pos : ∀ (a : α) (b : β), 0 < (W a).real {b}) (y : β) :

0 < (MeasureTheory.Measure.map (iidYs 0) (iidAmbientMeasure p W)).real {y}

Positivity of the output marginal: 0 < (μ.map (iidYs 0)).real {y}. Requires input positivity and channel positivity.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.iidAmbient_joint_real_singleton_pos

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (hp_pos : ∀ (a : α), 0 < p.real {a}) (hW_pos : ∀ (a : α) (b : β), 0 < (W a).real {b}) (q : α × β) :

0 < (MeasureTheory.Measure.map (jointSequence iidXs iidYs 0) (iidAmbientMeasure p W)).real {q}

Positivity of the joint marginal: 0 < (μ.map (jointSequence iidXs iidYs 0)).real {(x, y)}. Requires input + channel positivity.

Used by