InformationTheory.Shannon.BroadcastChannel.Marton.MarkovCore.Prelim

Imports 3

Marton's inner bound — coordinate laws shared by the two receivers #

The conditional AEP of the Marton ensemble is proved once per receiver, and the two proofs share the facts about the per-coordinate law that do not see the receiver index: the singleton masses of martonJointDistribution, its (V₁, V₂)- and ((V₁, V₂), X)-marginals, and the identity rewriting a sum against a pushed-forward law as a sum against the source law. Radius monotonicity of the strongly typical sets is collected here as well, because an assembly consuming both receivers pins its blocks at the minimum of the two radii and has to reopen each pin at the radius its own receiver asks for.

Main statements #

sum_map_real_singleton_mul — a finite sum of a statistic against a pushed-forward law equals the sum of its pullback against the source law.
martonJointDistribution_real_singleton — the mass the per-coordinate law puts on a quintuple factors as pV{v} · K(v){x} · W(x){y}.
martonJointDistribution_map_VX — the ((V₁, V₂), X)-marginal of the per-coordinate law is pV ⊗ₘ K.
marton_map_V₁V₂ — the ambient law of the auxiliary pair coordinate is pV.
stronglyTypicalSet_mono_radius and jointStronglyTypicalSet_mono_radius — the strongly typical sets grow with the radius.

Sums against a pushed-forward law #

theorem

InformationTheory.Shannon.BroadcastChannel.Marton.sum_map_real_singleton_mul

source

{Ω : Type u_6} {γ : Type u_7} [Fintype Ω] [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure P] (g : Ω → γ) (hg : Measurable g) (f : γ → ℝ) :

∑ c : γ, (MeasureTheory.Measure.map g P).real {c} * f c = ∑ z : Ω, P.real {z} * f (g z)

Used by

Singleton masses of the per-coordinate law #

theorem

InformationTheory.Shannon.BroadcastChannel.Marton.martonJointDistribution_real_singleton

source

{V₁ : Type u_1} {V₂ : Type u_2} {α : Type u_3} {β₁ : Type u_4} {β₂ : Type u_5} [Fintype V₁] [DecidableEq V₁] [Nonempty V₁] [MeasurableSpace V₁] [MeasurableSingletonClass V₁] [Fintype V₂] [DecidableEq V₂] [Nonempty V₂] [MeasurableSpace V₂] [MeasurableSingletonClass V₂] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β₁] [DecidableEq β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [Fintype β₂] [DecidableEq β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] (pV : MeasureTheory.Measure (V₁ × V₂)) [MeasureTheory.IsProbabilityMeasure pV] (K : ProbabilityTheory.Kernel (V₁ × V₂) α) [ProbabilityTheory.IsMarkovKernel K] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] (v : V₁ × V₂) (x : α) (y : β₁ × β₂) :

(martonJointDistribution pV K W).real {(v.1, v.2, x, y.1, y.2)} = pV.real {v} * (K v).real {x} * (W x).real {y}

Used by

Marginals of the per-coordinate law #

theorem

InformationTheory.Shannon.BroadcastChannel.Marton.martonJointDistribution_map_VX

source

MeasureTheory.Measure.map (fun (q : V₁ × V₂ × α × β₁ × β₂) => ((q.1, q.2.1), q.2.2.1)) (martonJointDistribution pV K W) = pV.compProd K

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.Marton.marton_map_V₁V₂

source

MeasureTheory.Measure.map (ChannelCoding.jointSequence martonV₁s martonV₂s 0) (martonAmbientMeasure pV K W) = pV

Used by

Radius monotonicity of the strongly typical sets #

theorem

InformationTheory.Shannon.BroadcastChannel.Marton.stronglyTypicalSet_mono_radius

source

{Ω : Type u_6} [MeasurableSpace Ω] {γ : Type u_7} [Fintype γ] [DecidableEq γ] [Nonempty γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → γ) (n : ℕ) {ε ε' : ℝ} (hε : ε ≤ ε') :

stronglyTypicalSet μ Xs n ε ⊆ stronglyTypicalSet μ Xs n ε'

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.Marton.jointStronglyTypicalSet_mono_radius

source

{Ω : Type u_6} [MeasurableSpace Ω] {γ : Type u_7} [Fintype γ] [DecidableEq γ] [Nonempty γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] {δ : Type u_8} [Fintype δ] [DecidableEq δ] [Nonempty δ] [MeasurableSpace δ] [MeasurableSingletonClass δ] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → γ) (Ys : ℕ → Ω → δ) (n : ℕ) {ε ε' : ℝ} (hε : ε ≤ ε') :

jointStronglyTypicalSet μ Xs Ys n ε ⊆ jointStronglyTypicalSet μ Xs Ys n ε'

Used by