InformationTheory.Shannon.BroadcastChannel.Marton.Setup
Marton's inner bound — five-variable ambient setup #
The random-coding ensemble behind Marton's inner bound carries a pair of auxiliary variables
(V₁, V₂), one per receiver, so the per-coordinate law is a quintuple (V₁, V₂, X, Y₁, Y₂)
rather than the quadruple (U, X, Y₁, Y₂) of superposition coding. This file builds that law
from a joint auxiliary distribution pV on V₁ × V₂, an input kernel K : Kernel (V₁ × V₂) α
and a broadcast channel W, together with its i.i.d. ambient measure, the coordinate facts
consumed downstream, and the three informations appearing in the region inequalities.
The input is produced by a general kernel K rather than a deterministic map x = f(v₁, v₂):
a deterministic kernel puts zero mass off its image, which is incompatible with the full-support
hypotheses hpV / hK / hW that every typicality bound in this development requires.
Main definitions #
martonJointDistribution pV K W— the per-coordinate law onV₁ × V₂ × α × β₁ × β₂.martonAmbientMeasure pV K W— its i.i.d. ambient measure onℕ → V₁ × V₂ × α × β₁ × β₂.martonInfo₁/martonInfo₂/martonInfoV₁V₂— the informationsI(V₁; Y₁),I(V₂; Y₂)andI(V₁; V₂)of the per-coordinate law, in entropy-difference form.
Implementation notes #
The informations are entropy differences over ℝ rather than InformationTheory.Shannon.mutualInfo
(valued in ℝ≥0∞), matching the form in which the typicality bounds of this development state
their exponents.
Per-coordinate joint distribution #
InformationTheory.Shannon.BroadcastChannel.Marton.martonJointDistribution
source{V₁ : Type u_1}
{V₂ : Type u_2}
{α : Type u_3}
{β₁ : Type u_4}
{β₂ : Type u_5}
[MeasurableSpace V₁]
[MeasurableSpace V₂]
[MeasurableSpace α]
[MeasurableSpace β₁]
[MeasurableSpace β₂]
(pV : MeasureTheory.Measure (V₁ × V₂))
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
(W : BCChannel α β₁ β₂)
:
MeasureTheory.Measure (V₁ × V₂ × α × β₁ × β₂)
The per-coordinate Marton joint law on V₁ × V₂ × α × β₁ × β₂: the compProd chain
pV → K → W ((V₁, V₂) ∼ pV, X ∣ (V₁, V₂) ∼ K, (Y₁, Y₂) ∣ X ∼ W), reshaped from the
left-nested ((V₁ × V₂) × α) × (β₁ × β₂) to the right-nested quintuple. Two reassociations
are needed, one more than for the four-variable superposition law.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonJointDistribution.instIsProbabilityMeasure
source{V₁ : Type u_1}
{V₂ : Type u_2}
{α : Type u_3}
{β₁ : Type u_4}
{β₂ : Type u_5}
[MeasurableSpace V₁]
[MeasurableSpace V₂]
[MeasurableSpace α]
[MeasurableSpace β₁]
[MeasurableSpace β₂]
(pV : MeasureTheory.Measure (V₁ × V₂))
[MeasureTheory.IsProbabilityMeasure pV]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
[ProbabilityTheory.IsMarkovKernel K]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
:
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonJointDistribution_map_V
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]
:
MeasureTheory.Measure.map (fun (q : V₁ × V₂ × α × β₁ × β₂) => (q.1, q.2.1)) (martonJointDistribution pV K W) = pV
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonJointDistribution_singleton_pos
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]
(hpV : ∀ (v : V₁ × V₂), 0 < pV.real {v})
(hK : ∀ (v : V₁ × V₂) (a : α), 0 < (K v).real {a})
(hW : ∀ (a : α) (b : β₁ × β₂), 0 < (W a).real {b})
(q : V₁ × V₂ × α × β₁ × β₂)
:
Used by
I.i.d. ambient measure on ℕ → V₁ × V₂ × α × β₁ × β₂ #
InformationTheory.Shannon.BroadcastChannel.Marton.martonAmbientMeasure
source{V₁ : Type u_1}
{V₂ : Type u_2}
{α : Type u_3}
{β₁ : Type u_4}
{β₂ : Type u_5}
[MeasurableSpace V₁]
[MeasurableSpace V₂]
[MeasurableSpace α]
[MeasurableSpace β₁]
[MeasurableSpace β₂]
(pV : MeasureTheory.Measure (V₁ × V₂))
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
(W : BCChannel α β₁ β₂)
:
The i.i.d. Marton ambient measure:
Measure.infinitePi (fun _ => martonJointDistribution pV K W).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonAmbientMeasure.instIsProbabilityMeasure
source{V₁ : Type u_1}
{V₂ : Type u_2}
{α : Type u_3}
{β₁ : Type u_4}
{β₂ : Type u_5}
[MeasurableSpace V₁]
[MeasurableSpace V₂]
[MeasurableSpace α]
[MeasurableSpace β₁]
[MeasurableSpace β₂]
(pV : MeasureTheory.Measure (V₁ × V₂))
[MeasureTheory.IsProbabilityMeasure pV]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
[ProbabilityTheory.IsMarkovKernel K]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
:
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonV₁s
sourceThe first auxiliary coordinate ω ↦ (ω i).1.
Equations
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonV₂s
sourceThe second auxiliary coordinate ω ↦ (ω i).2.1.
Equations
- InformationTheory.Shannon.BroadcastChannel.Marton.martonV₂s i ω = (ω i).2.1
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonXs
sourceThe channel input coordinate ω ↦ (ω i).2.2.1.
Equations
- InformationTheory.Shannon.BroadcastChannel.Marton.martonXs i ω = (ω i).2.2.1
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonY₁s
sourceThe first output coordinate ω ↦ (ω i).2.2.2.1.
Equations
- InformationTheory.Shannon.BroadcastChannel.Marton.martonY₁s i ω = (ω i).2.2.2.1
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonY₂s
sourceThe second output coordinate ω ↦ (ω i).2.2.2.2.
Equations
- InformationTheory.Shannon.BroadcastChannel.Marton.martonY₂s i ω = (ω i).2.2.2.2
Instances For
Used by
Coordinate facts for the Marton ambient measure #
InformationTheory.Shannon.BroadcastChannel.Marton.martonAmbient_map_coord
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 β₂]
{γ : Type u_6}
[MeasurableSpace γ]
(pV : MeasureTheory.Measure (V₁ × V₂))
[MeasureTheory.IsProbabilityMeasure pV]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
[ProbabilityTheory.IsMarkovKernel K]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(g : V₁ × V₂ × α × β₁ × β₂ → γ)
(hg : Measurable g)
(i : ℕ)
:
MeasureTheory.Measure.map (fun (ω : ℕ → V₁ × V₂ × α × β₁ × β₂) => g (ω i)) (martonAmbientMeasure pV K W) = MeasureTheory.Measure.map g (martonJointDistribution pV K W)
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonAmbient_iIndepFun_coord
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 β₂]
{γ : Type u_6}
[MeasurableSpace γ]
(pV : MeasureTheory.Measure (V₁ × V₂))
[MeasureTheory.IsProbabilityMeasure pV]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
[ProbabilityTheory.IsMarkovKernel K]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(g : V₁ × V₂ × α × β₁ × β₂ → γ)
(hg : Measurable g)
:
ProbabilityTheory.iIndepFun (fun (i : ℕ) (ω : ℕ → V₁ × V₂ × α × β₁ × β₂) => g (ω i)) (martonAmbientMeasure pV K W)
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonAmbient_identDistrib_coord
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 β₂]
{γ : Type u_6}
[MeasurableSpace γ]
(pV : MeasureTheory.Measure (V₁ × V₂))
[MeasureTheory.IsProbabilityMeasure pV]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
[ProbabilityTheory.IsMarkovKernel K]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(g : V₁ × V₂ × α × β₁ × β₂ → γ)
(hg : Measurable g)
(i : ℕ)
:
ProbabilityTheory.IdentDistrib (fun (ω : ℕ → V₁ × V₂ × α × β₁ × β₂) => g (ω i))
(fun (ω : ℕ → V₁ × V₂ × α × β₁ × β₂) => g (ω 0)) (martonAmbientMeasure pV K W) (martonAmbientMeasure pV K W)
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonAmbient_entropy_coord
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 β₂]
{γ : Type u_6}
[Fintype γ]
[Nonempty γ]
[MeasurableSpace γ]
[MeasurableSingletonClass γ]
(pV : MeasureTheory.Measure (V₁ × V₂))
[MeasureTheory.IsProbabilityMeasure pV]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
[ProbabilityTheory.IsMarkovKernel K]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(g : V₁ × V₂ × α × β₁ × β₂ → γ)
(hg : Measurable g)
(i : ℕ)
:
(entropy (martonAmbientMeasure pV K W) fun (ω : ℕ → V₁ × V₂ × α × β₁ × β₂) => g (ω i)) = entropy (martonJointDistribution pV K W) g
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonAmbient_coord_marginal_pos
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 β₂]
{γ : Type u_6}
[MeasurableSpace γ]
[MeasurableSingletonClass γ]
(pV : MeasureTheory.Measure (V₁ × V₂))
[MeasureTheory.IsProbabilityMeasure pV]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
[ProbabilityTheory.IsMarkovKernel K]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(hpV : ∀ (v : V₁ × V₂), 0 < pV.real {v})
(hK : ∀ (v : V₁ × V₂) (a : α), 0 < (K v).real {a})
(hW : ∀ (a : α) (b : β₁ × β₂), 0 < (W a).real {b})
(g : V₁ × V₂ × α × β₁ × β₂ → γ)
(hg : Measurable g)
(i : ℕ)
(c : γ)
(r : V₁ × V₂ × α × β₁ × β₂)
(hr : g r = c)
:
Used by
The three informations of the region inequalities #
InformationTheory.Shannon.BroadcastChannel.Marton.martonInfo₁
source{V₁ : Type u_1}
{V₂ : Type u_2}
{α : Type u_3}
{β₁ : Type u_4}
{β₂ : Type u_5}
[Fintype V₁]
[MeasurableSpace V₁]
[MeasurableSpace V₂]
[MeasurableSpace α]
[Fintype β₁]
[MeasurableSpace β₁]
[MeasurableSpace β₂]
(pV : MeasureTheory.Measure (V₁ × V₂))
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
(W : BCChannel α β₁ β₂)
:
The first-receiver information I(V₁; Y₁) = H(V₁) + H(Y₁) − H(V₁, Y₁) of the
per-coordinate Marton joint law.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonInfo₂
source{V₁ : Type u_1}
{V₂ : Type u_2}
{α : Type u_3}
{β₁ : Type u_4}
{β₂ : Type u_5}
[MeasurableSpace V₁]
[Fintype V₂]
[MeasurableSpace V₂]
[MeasurableSpace α]
[MeasurableSpace β₁]
[Fintype β₂]
[MeasurableSpace β₂]
(pV : MeasureTheory.Measure (V₁ × V₂))
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
(W : BCChannel α β₁ β₂)
:
The second-receiver information I(V₂; Y₂) = H(V₂) + H(Y₂) − H(V₂, Y₂) of the
per-coordinate Marton joint law.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonInfoV₁V₂
source{V₁ : Type u_1}
{V₂ : Type u_2}
{α : Type u_3}
{β₁ : Type u_4}
{β₂ : Type u_5}
[Fintype V₁]
[MeasurableSpace V₁]
[Fintype V₂]
[MeasurableSpace V₂]
[MeasurableSpace α]
[MeasurableSpace β₁]
[MeasurableSpace β₂]
(pV : MeasureTheory.Measure (V₁ × V₂))
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
(W : BCChannel α β₁ β₂)
:
The auxiliary-variable dependence I(V₁; V₂) = H(V₁) + H(V₂) − H(V₁, V₂) of the
per-coordinate Marton joint law. This is the penalty subtracted from the sum rate: it is the
rate at which the two subcodebooks have to be over-provisioned for a jointly typical pair to
exist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonInfo₁_eq_zero_of_subsingleton
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 β₂]
[Subsingleton V₁]
(pV : MeasureTheory.Measure (V₁ × V₂))
[MeasureTheory.IsProbabilityMeasure pV]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
[ProbabilityTheory.IsMarkovKernel K]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
:
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonInfoV₁V₂_eq_zero_of_prod
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 β₂]
(p₁ : MeasureTheory.Measure V₁)
[MeasureTheory.IsProbabilityMeasure p₁]
(p₂ : MeasureTheory.Measure V₂)
[MeasureTheory.IsProbabilityMeasure p₂]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
[ProbabilityTheory.IsMarkovKernel K]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
: