InformationTheory.Shannon.BroadcastChannel.OuterBoundUV.MartonBridge
Broadcast channel — Marton's inner-bound law as a UV channel law #
Marton's inner bound and the UV outer bound both live over five-tuple laws
(V₁, V₂, X, Y₁, Y₂) of the same type, but they index the two auxiliaries in opposite order: an
outer information slot pairs the second auxiliary with the first receiver, while an inner one
pairs the first auxiliary with it. This file puts the two on one index. The Marton joint law is
a channel law of W; exchanging its two auxiliaries preserves that, and re-encoding the two
finite auxiliary alphabets into ℕ lands the law in the family indexing the UV outer region.
The two corner informations of the inner bound are then the corresponding slots of the exchanged
law, and its auxiliary dependence is the mutual information of the two auxiliaries of the joint
law. The sum rate of the inner bound is bounded by both sum-rate slots of the outer bound, so
the inner quadrilateral is contained in the outer region.
Main definitions #
natIndex X— the index of a letter of the finite alphabetX, as a natural number.martonAuxSwapLaw— the Marton joint law with its two auxiliaries exchanged.martonUVLaw— the exchanged law re-encoded over the natural-number auxiliaries indexingbcOuterRegionUV.
Main statements #
martonJointDistribution_isUVChannelLaw— the Marton joint law is a channel law ofW. No support hypothesis on the input law, the auxiliary kernel or the channel is needed.martonUVLaw_isUVChannelLaw— so is its exchanged and re-encoded form, which is therefore one of the laws the union definingbcOuterRegionUVranges over.martonInfo₁_eq_uvInfo₁_toRealandmartonInfo₂_eq_uvInfo₂_toReal— the two corner informations of the inner bound, defined as entropy differences overℝ, are the corresponding slots of the exchanged law.marton_region_subset_uv— Marton's inner-bound quadrilateral is contained in the UV outer region, again with no support hypothesis.
Implementation notes #
IsUVChannelLaw reads the two auxiliaries and the input letter as one block, so it does not see
their order: the Marton law satisfies it with no exchange at all, and the exchange enters only
where an information slot is read. The exchanged law is given a name of its own, and an
IsProbabilityMeasure instance, because the slot lemmas of the re-encoding need that instance at
a law that is not syntactically a martonJointDistribution.
The Marton joint law is a channel law #
InformationTheory.Shannon.BroadcastChannel.Marton.martonJointDistribution_isUVChannelLaw
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]
:
IsUVChannelLaw W (martonJointDistribution pV K W)
The Marton joint law is a channel law of W: its outputs are drawn from the channel at the
input letter and the two auxiliaries reach them through that letter only. The law is built as a
composition-product chain ending in W, so this holds with no support hypothesis on the input
law, on the auxiliary kernel or on the channel.
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonAuxSwapLaw
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 Marton joint law with its two auxiliaries exchanged, which is the order in which the information slots of the UV outer bound read them.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonAuxSwapLaw.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.martonAuxSwapLaw_isUVChannelLaw
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]
:
IsUVChannelLaw W (martonAuxSwapLaw pV K W)
Used by
The natural-number auxiliaries of the outer region #
InformationTheory.Shannon.BroadcastChannel.Marton.natIndex
sourceThe index of a letter of a finite alphabet, as a natural number. This is the re-encoding
carrying a law over finite auxiliary alphabets to the natural-number auxiliaries over which the
union defining bcOuterRegionUV is taken. Encodable.encode is the same map up to the arbitrary
choice of an ordering, but a finite alphabet carries no Encodable instance, and its decoder is
Option-valued whereas the slot lemmas of the re-encoding take a total left inverse.
Equations
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.natIndex_injective
sourceUsed by
InformationTheory.Shannon.BroadcastChannel.Marton.martonUVLaw
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 exchanged Marton joint law, re-encoded over the natural-number auxiliaries indexing the UV outer region.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonUVLaw.instIsProbabilityMeasure
source{V₁ : Type u_1}
{V₂ : Type u_2}
{α : Type u_3}
{β₁ : Type u_4}
{β₂ : Type u_5}
[Fintype V₁]
[MeasurableSpace V₁]
[MeasurableSingletonClass V₁]
[Fintype V₂]
[MeasurableSpace V₂]
[MeasurableSingletonClass 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.martonUVLaw_isUVChannelLaw
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]
:
IsUVChannelLaw W (martonUVLaw pV K W)
The exchanged and re-encoded Marton joint law is a channel law of W, hence one of the laws
the union defining bcOuterRegionUV ranges over.
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.uvInfo₁_martonUVLaw
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]
:
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.uvInfo₂_martonUVLaw
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]
:
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.uvInfoSum₂_martonUVLaw
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]
:
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.uvInfoSum₁_martonUVLaw
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]
:
Used by
The informations of the inner bound as slots of the exchanged law #
InformationTheory.Shannon.BroadcastChannel.Marton.martonInfo₁_eq_uvInfo₁_toReal
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]
:
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonInfo₂_eq_uvInfo₂_toReal
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]
:
Used by
The Markov chains carried by the Marton joint law #
The sum-rate inequalities #
InformationTheory.Shannon.BroadcastChannel.Marton.martonInfo₁_sub_martonInfoV₁V₂_le
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]
:
martonInfo₁ pV K W - martonInfoV₁V₂ pV K W ≤ (condMutualInfo (martonAuxSwapLaw pV K W) (fun (q : V₂ × V₁ × α × β₁ × β₂) => q.2.2.1)
(fun (q : V₂ × V₁ × α × β₁ × β₂) => q.2.2.2.1) fun (q : V₂ × V₁ × α × β₁ × β₂) => q.1).toReal
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonInfo₂_sub_martonInfoV₁V₂_le
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]
:
martonInfo₂ pV K W - martonInfoV₁V₂ pV K W ≤ (condMutualInfo (martonAuxSwapLaw pV K W) (fun (q : V₂ × V₁ × α × β₁ × β₂) => q.2.2.1)
(fun (q : V₂ × V₁ × α × β₁ × β₂) => q.2.2.2.2) fun (q : V₂ × V₁ × α × β₁ × β₂) => q.2.1).toReal
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonInfo₁_add_martonInfo₂_sub_martonInfoV₁V₂_le_uvInfoSum₂_toReal
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]
:
martonInfo₁ pV K W + martonInfo₂ pV K W - martonInfoV₁V₂ pV K W ≤ (uvInfoSum₂ (martonAuxSwapLaw pV K W)).toReal
Used by
InformationTheory.Shannon.BroadcastChannel.Marton.martonInfo₁_add_martonInfo₂_sub_martonInfoV₁V₂_le_uvInfoSum₁_toReal
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]
:
martonInfo₁ pV K W + martonInfo₂ pV K W - martonInfoV₁V₂ pV K W ≤ (uvInfoSum₁ (martonAuxSwapLaw pV K W)).toReal
Used by
The inner quadrilateral inside the outer region #
InformationTheory.Shannon.BroadcastChannel.Marton.marton_region_subset_uv
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]
:
Marton's inner-bound quadrilateral is contained in the UV outer region: the exchanged and re-encoded Marton joint law is one of the laws the outer union ranges over, and the three informations of the inner bound meet its four constraints at that law. No support hypothesis on the input law, the auxiliary kernel or the channel is needed.