InformationTheory.Shannon.BroadcastChannel.MartonFullSupport
Broadcast channel — Marton's inner bound without the auxiliary support hypotheses #
marton_region_subset_capacity asks the auxiliary law, the input kernel and the channel to
charge every letter, since the random-coding argument behind it counts jointly typical
sequences. Only the channel hypothesis is intrinsic: an auxiliary law or an input kernel that
misses a letter is a limit of ones that do not, and the three informations of the quadrilateral
are continuous along such a smoothing, because on a finite alphabet each of them is a fixed
polynomial expression in the singleton masses composed with Real.negMulLog. This file runs
that limit and removes the two auxiliary hypotheses.
Main definitions #
martonMixKernel K κ₀ ε— the input kernel smoothed toward a fixed anchor measure, letter by letter, by the clamped-weight mixtureInformationTheory.mixLaw.
Main statements #
marton_region_subset_capacity_of_channel_fullSupport— a Marton quadrilateral is contained in the operational capacity region, under a support hypothesis on the channel alone.martonRegionUnion_subset_capacity— the whole union, not only its full-support part, is contained in the operational capacity region.
Smoothing the input kernel #
InformationTheory.Shannon.BroadcastChannel.Marton.martonMixKernel
source{V₁ : Type u_1}
{V₂ : Type u_2}
[Fintype V₁]
[MeasurableSpace V₁]
[MeasurableSingletonClass V₁]
[Fintype V₂]
[MeasurableSpace V₂]
[MeasurableSingletonClass V₂]
{α : Type u_3}
[MeasurableSpace α]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
(κ₀ : MeasureTheory.Measure α)
(ε : ℝ)
:
ProbabilityTheory.Kernel (V₁ × V₂) α
The input kernel smoothed toward a fixed anchor measure κ₀, letter by letter:
martonMixKernel K κ₀ ε v = (1 - ε) • K v + ε • κ₀ with the weight clamped to [0, 1]. For
ε > 0 and a full-support anchor every letter is charged, and at ε = 0 the kernel is K.
Equations
- InformationTheory.Shannon.BroadcastChannel.Marton.martonMixKernel K κ₀ ε = ProbabilityTheory.Kernel.ofFunOfCountable fun (v : V₁ × V₂) => InformationTheory.mixLaw (K v) κ₀ ε
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonMixKernel_apply
source{V₁ : Type u_1}
{V₂ : Type u_2}
[Fintype V₁]
[MeasurableSpace V₁]
[MeasurableSingletonClass V₁]
[Fintype V₂]
[MeasurableSpace V₂]
[MeasurableSingletonClass V₂]
{α : Type u_3}
[MeasurableSpace α]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
(κ₀ : MeasureTheory.Measure α)
(ε : ℝ)
(v : V₁ × V₂)
:
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonMixKernel.instIsMarkovKernel
source{V₁ : Type u_1}
{V₂ : Type u_2}
[Fintype V₁]
[MeasurableSpace V₁]
[MeasurableSingletonClass V₁]
[Fintype V₂]
[MeasurableSpace V₂]
[MeasurableSingletonClass V₂]
{α : Type u_3}
[MeasurableSpace α]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
[ProbabilityTheory.IsMarkovKernel K]
(κ₀ : MeasureTheory.Measure α)
[MeasureTheory.IsProbabilityMeasure κ₀]
(ε : ℝ)
:
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonMixKernel_zero
source{V₁ : Type u_1}
{V₂ : Type u_2}
[Fintype V₁]
[MeasurableSpace V₁]
[MeasurableSingletonClass V₁]
[Fintype V₂]
[MeasurableSpace V₂]
[MeasurableSingletonClass V₂]
{α : Type u_3}
[MeasurableSpace α]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
(κ₀ : MeasureTheory.Measure α)
:
Used by
Continuity of the three informations along the smoothing #
InformationTheory.Shannon.BroadcastChannel.Marton.martonMixJoint_real_continuous
source{V₁ : Type u_1}
{V₂ : Type u_2}
{α : Type u_3}
{β₁ : Type u_4}
{β₂ : Type u_5}
[Fintype V₁]
[Nonempty V₁]
[MeasurableSpace V₁]
[MeasurableSingletonClass V₁]
[Fintype V₂]
[Nonempty V₂]
[MeasurableSpace V₂]
[MeasurableSingletonClass V₂]
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
(pV μ₀ : MeasureTheory.Measure (V₁ × V₂))
[MeasureTheory.IsProbabilityMeasure pV]
[MeasureTheory.IsProbabilityMeasure μ₀]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
[ProbabilityTheory.IsMarkovKernel K]
(κ₀ : MeasureTheory.Measure α)
[MeasureTheory.IsProbabilityMeasure κ₀]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(q : V₁ × V₂ × α × β₁ × β₂)
:
Continuous fun (ε : ℝ) => (martonJointDistribution (mixLaw pV μ₀ ε) (martonMixKernel K κ₀ ε) W).real {q}
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonMixJoint_map_real_continuous
source{V₁ : Type u_1}
{V₂ : Type u_2}
{α : Type u_3}
{β₁ : Type u_4}
{β₂ : Type u_5}
[Fintype V₁]
[Nonempty V₁]
[MeasurableSpace V₁]
[MeasurableSingletonClass V₁]
[Fintype V₂]
[Nonempty V₂]
[MeasurableSpace V₂]
[MeasurableSingletonClass V₂]
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
(pV μ₀ : MeasureTheory.Measure (V₁ × V₂))
[MeasureTheory.IsProbabilityMeasure pV]
[MeasureTheory.IsProbabilityMeasure μ₀]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
[ProbabilityTheory.IsMarkovKernel K]
(κ₀ : MeasureTheory.Measure α)
[MeasureTheory.IsProbabilityMeasure κ₀]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
{γ : Type u_6}
[MeasurableSpace γ]
[MeasurableSingletonClass γ]
(f : V₁ × V₂ × α × β₁ × β₂ → γ)
(hf : Measurable f)
(x : γ)
:
Continuous fun (ε : ℝ) =>
(MeasureTheory.Measure.map f (martonJointDistribution (mixLaw pV μ₀ ε) (martonMixKernel K κ₀ ε) W)).real {x}
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonMix_entropy_continuous
source{V₁ : Type u_1}
{V₂ : Type u_2}
{α : Type u_3}
{β₁ : Type u_4}
{β₂ : Type u_5}
[Fintype V₁]
[Nonempty V₁]
[MeasurableSpace V₁]
[MeasurableSingletonClass V₁]
[Fintype V₂]
[Nonempty V₂]
[MeasurableSpace V₂]
[MeasurableSingletonClass V₂]
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
(pV μ₀ : MeasureTheory.Measure (V₁ × V₂))
[MeasureTheory.IsProbabilityMeasure pV]
[MeasureTheory.IsProbabilityMeasure μ₀]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
[ProbabilityTheory.IsMarkovKernel K]
(κ₀ : MeasureTheory.Measure α)
[MeasureTheory.IsProbabilityMeasure κ₀]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
{γ : Type u_6}
[Fintype γ]
[MeasurableSpace γ]
[MeasurableSingletonClass γ]
(f : V₁ × V₂ × α × β₁ × β₂ → γ)
(hf : Measurable f)
:
Continuous fun (ε : ℝ) => entropy (martonJointDistribution (mixLaw pV μ₀ ε) (martonMixKernel K κ₀ ε) W) f
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonInfo₁_mix_continuous
source{V₁ : Type u_1}
{V₂ : Type u_2}
{α : Type u_3}
{β₁ : Type u_4}
{β₂ : Type u_5}
[Fintype V₁]
[Nonempty V₁]
[MeasurableSpace V₁]
[MeasurableSingletonClass V₁]
[Fintype V₂]
[Nonempty V₂]
[MeasurableSpace V₂]
[MeasurableSingletonClass V₂]
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
(pV μ₀ : MeasureTheory.Measure (V₁ × V₂))
[MeasureTheory.IsProbabilityMeasure pV]
[MeasureTheory.IsProbabilityMeasure μ₀]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
[ProbabilityTheory.IsMarkovKernel K]
(κ₀ : MeasureTheory.Measure α)
[MeasureTheory.IsProbabilityMeasure κ₀]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
:
Continuous fun (ε : ℝ) => martonInfo₁ (mixLaw pV μ₀ ε) (martonMixKernel K κ₀ ε) W
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonInfo₂_mix_continuous
source{V₁ : Type u_1}
{V₂ : Type u_2}
{α : Type u_3}
{β₁ : Type u_4}
{β₂ : Type u_5}
[Fintype V₁]
[Nonempty V₁]
[MeasurableSpace V₁]
[MeasurableSingletonClass V₁]
[Fintype V₂]
[Nonempty V₂]
[MeasurableSpace V₂]
[MeasurableSingletonClass V₂]
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
(pV μ₀ : MeasureTheory.Measure (V₁ × V₂))
[MeasureTheory.IsProbabilityMeasure pV]
[MeasureTheory.IsProbabilityMeasure μ₀]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
[ProbabilityTheory.IsMarkovKernel K]
(κ₀ : MeasureTheory.Measure α)
[MeasureTheory.IsProbabilityMeasure κ₀]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
:
Continuous fun (ε : ℝ) => martonInfo₂ (mixLaw pV μ₀ ε) (martonMixKernel K κ₀ ε) W
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonInfoV₁V₂_mix_continuous
source{V₁ : Type u_1}
{V₂ : Type u_2}
{α : Type u_3}
{β₁ : Type u_4}
{β₂ : Type u_5}
[Fintype V₁]
[Nonempty V₁]
[MeasurableSpace V₁]
[MeasurableSingletonClass V₁]
[Fintype V₂]
[Nonempty V₂]
[MeasurableSpace V₂]
[MeasurableSingletonClass V₂]
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
(pV μ₀ : MeasureTheory.Measure (V₁ × V₂))
[MeasureTheory.IsProbabilityMeasure pV]
[MeasureTheory.IsProbabilityMeasure μ₀]
(K : ProbabilityTheory.Kernel (V₁ × V₂) α)
[ProbabilityTheory.IsMarkovKernel K]
(κ₀ : MeasureTheory.Measure α)
[MeasureTheory.IsProbabilityMeasure κ₀]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
:
Continuous fun (ε : ℝ) => martonInfoV₁V₂ (mixLaw pV μ₀ ε) (martonMixKernel K κ₀ ε) W
Used by
The inner bound under a channel hypothesis alone #
InformationTheory.Shannon.BroadcastChannel.Marton.marton_region_subset_capacity_of_channel_fullSupport
source{V₁ : Type u_1}
{V₂ : Type u_2}
{α : Type u_3}
{β₁ : Type u_4}
{β₂ : Type u_5}
[Fintype V₁]
[Nonempty V₁]
[MeasurableSpace V₁]
[MeasurableSingletonClass V₁]
[Fintype V₂]
[Nonempty V₂]
[MeasurableSpace V₂]
[MeasurableSingletonClass V₂]
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[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]
(hW : ∀ (a : α) (b : β₁ × β₂), 0 < (W a).real {b})
:
Marton's inner bound sits inside the operational capacity region under a support hypothesis
on the channel alone. Smoothing the auxiliary law and the input kernel toward the uniform ones
makes them charge every letter, and the three informations of the quadrilateral are continuous
along that smoothing, so the two support hypotheses that marton_region_subset_capacity asks of
them are not needed. The channel hypothesis hW is a regularity precondition of the coding
argument and carries no part of it.
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonRegionUnion_subset_capacity
source{α : Type u}
{β₁ : Type u_1}
{β₂ : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(hW : ∀ (a : α) (b : β₁ × β₂), 0 < (W a).real {b})
:
Marton's inner bound is achievable in full: the union over all auxiliary laws and input kernels, not only over the full-support ones, is contained in the operational capacity region. Only the channel is required to have full support.