InformationTheory.Shannon.BroadcastChannel.OuterBoundUV.Quantization
Broadcast channel — truncating the countable auxiliary of the UV outer region #
The UV outer region is indexed by five-tuple laws whose two auxiliaries range over ℕ, while an
inner bound reads its auxiliary off a finite alphabet. Truncating the first auxiliary at a level
m, folding every letter at or above m into a single one, moves a law of the outer region onto
the finite alphabet Fin (m + 1), and the two slots the truncated auxiliary appears in move in
opposite directions.
The conditional slot I(X; Y₁ ∣ U) can only grow: the truncated auxiliary is a function of the
original one, and a channel law makes the auxiliary reach the first output through the input
letter only, so the extra conditioning the original auxiliary would supply is already spent. The
corner slot I(U; Y₂) can shrink, by exactly the information the original auxiliary still carries
once the truncated one is known. That information lives on the fibers of the truncation, all but
one of which pin the auxiliary to a single letter, so it is carried by the tail alone and the
finite output alphabet caps it by log |β₂|.
Main definitions #
uvQuantize m— the truncating quantizer of the countable auxiliary.uvQuantizeLaw ν m— the five-tuple law with its first auxiliary truncated at levelm.uvQuantizeSlack ν m— the tail mass of the auxiliary timeslog |β₂|.
Main statements #
uvQuantizeLaw_isUVChannelLaw— truncating the auxiliary keeps a channel law a channel law.uvInfo₂_le_uvQuantizeLaw_add_slackanduvInfoSum₂_le_uvQuantizeLaw_add_slack— the receiver-2 corner slot and the sum-rate slot lose at most the slack under the truncation.tendsto_uvQuantizeSlack— the slack vanishes as the truncation level grows.uvInfo₂_ne_topanduvInfoSum₂_ne_top— the two slots are finite even over a countable auxiliary, which is what lets the estimates be read in the reals.
Finiteness and monotonicity of the information slots #
Finiteness of the slots over a countable auxiliary #
InformationTheory.Shannon.BroadcastChannel.uvInfo₂_ne_top
source{α : Type u}
{β₁ : Type u_1}
{β₂ : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β₁]
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
{U : Type u_3}
{V : Type u_4}
[MeasurableSpace U]
[StandardBorelSpace U]
[Nonempty U]
[MeasurableSpace V]
(ν : MeasureTheory.Measure (U × V × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure ν]
:
Used by
InformationTheory.Shannon.BroadcastChannel.uvInfoSum₂_ne_top
source{α : Type u}
{β₁ : Type u_1}
{β₂ : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
{U : Type u_3}
{V : Type u_4}
[MeasurableSpace U]
[StandardBorelSpace U]
[Nonempty U]
[MeasurableSpace V]
(ν : MeasureTheory.Measure (U × V × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure ν]
:
Used by
Coarsening the conditioner of the sum-rate slot #
InformationTheory.Shannon.BroadcastChannel.IsUVChannelLaw.condMutualInfo_le_map_cond
source{α : Type u}
{β₁ : Type u_1}
{β₂ : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
{U : Type u_3}
{V : Type u_4}
[MeasurableSpace U]
[StandardBorelSpace U]
[Nonempty U]
[MeasurableSpace V]
[StandardBorelSpace V]
[Nonempty V]
{U' : Type u_5}
[MeasurableSpace U']
[StandardBorelSpace U']
[Nonempty U']
{W : BCChannel α β₁ β₂}
[ProbabilityTheory.IsMarkovKernel W]
{ν : MeasureTheory.Measure (U × V × α × β₁ × β₂)}
[MeasureTheory.IsProbabilityMeasure ν]
(h : IsUVChannelLaw W ν)
{f : U → U'}
(hf : Measurable f)
:
Used by
Truncating the countable auxiliary #
The truncating quantizer #
InformationTheory.Shannon.BroadcastChannel.uvQuantize
sourceThe truncating quantizer of the countable auxiliary: letters below the truncation level are kept and every letter at or above it is folded into the top one.
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.measurable_uvQuantize
sourceUsed by
InformationTheory.Shannon.BroadcastChannel.uvQuantize_down_eq_iff
sourceUsed by
InformationTheory.Shannon.BroadcastChannel.uvQuantizeLaw
source{α : Type u}
{β₁ : Type u_1}
{β₂ : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β₁]
[MeasurableSpace β₂]
(ν : MeasureTheory.Measure (ℕ × ℕ × α × β₁ × β₂))
(m : ℕ)
:
MeasureTheory.Measure (ULift.{u, 0} (Fin (m + 1)) × ℕ × α × β₁ × β₂)
The five-tuple law with its first auxiliary truncated at level m.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.uvQuantizeSlack
source{α : Type u}
{β₁ : Type u_1}
{β₂ : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β₁]
[Fintype β₂]
[MeasurableSpace β₂]
(ν : MeasureTheory.Measure (ℕ × ℕ × α × β₁ × β₂))
(m : ℕ)
:
The information the truncation can cost: the tail mass of the auxiliary times the largest entropy the second output alphabet can carry.
Equations
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.uvQuantizeLaw_isProbabilityMeasure
source{α : Type u}
{β₁ : Type u_1}
{β₂ : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β₁]
[MeasurableSpace β₂]
(ν : MeasureTheory.Measure (ℕ × ℕ × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure ν]
(m : ℕ)
:
Used by
InformationTheory.Shannon.BroadcastChannel.uvQuantizeLaw_isUVChannelLaw
source{α : Type u}
{β₁ : Type u_1}
{β₂ : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β₁]
[MeasurableSpace β₂]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
{ν : MeasureTheory.Measure (ℕ × ℕ × α × β₁ × β₂)}
[MeasureTheory.SFinite ν]
(h : IsUVChannelLaw W ν)
(m : ℕ)
:
IsUVChannelLaw W (uvQuantizeLaw ν m)
Used by
The slots of the truncated law #
InformationTheory.Shannon.BroadcastChannel.uvInfo₁_uvQuantizeLaw
source{α : Type u}
{β₁ : Type u_1}
{β₂ : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β₁]
[MeasurableSpace β₂]
(ν : MeasureTheory.Measure (ℕ × ℕ × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure ν]
(m : ℕ)
:
Used by
InformationTheory.Shannon.BroadcastChannel.uvInfo₂_uvQuantizeLaw
source{α : Type u}
{β₁ : Type u_1}
{β₂ : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β₁]
[MeasurableSpace β₂]
(ν : MeasureTheory.Measure (ℕ × ℕ × α × β₁ × β₂))
(m : ℕ)
:
Used by
InformationTheory.Shannon.BroadcastChannel.condMutualInfo_uvQuantizeLaw
source{α : Type u}
{β₁ : Type u_1}
{β₂ : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[MeasurableSpace β₂]
(ν : MeasureTheory.Measure (ℕ × ℕ × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure ν]
(m : ℕ)
:
(condMutualInfo (uvQuantizeLaw ν m) (fun (q : ULift.{u, 0} (Fin (m + 1)) × ℕ × α × β₁ × β₂) => q.2.2.1)
(fun (q : ULift.{u, 0} (Fin (m + 1)) × ℕ × α × β₁ × β₂) => q.2.2.2.1)
fun (q : ULift.{u, 0} (Fin (m + 1)) × ℕ × α × β₁ × β₂) => q.1) = condMutualInfo ν (fun (q : ℕ × ℕ × α × β₁ × β₂) => q.2.2.1) (fun (q : ℕ × ℕ × α × β₁ × β₂) => q.2.2.2.1)
fun (q : ℕ × ℕ × α × β₁ × β₂) => uvQuantize m q.1
Used by
InformationTheory.Shannon.BroadcastChannel.uvQuantizeSlack_ne_top
source{α : Type u}
{β₁ : Type u_1}
{β₂ : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β₁]
[Fintype β₂]
[MeasurableSpace β₂]
(ν : MeasureTheory.Measure (ℕ × ℕ × α × β₁ × β₂))
(m : ℕ)
[MeasureTheory.IsFiniteMeasure ν]
:
Used by
The tail estimate for the corner slot #
InformationTheory.Shannon.BroadcastChannel.ae_ae_uvQuantize_eq_fst
source{α : Type u}
{β₁ : Type u_1}
{β₂ : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
(ν : MeasureTheory.Measure (ℕ × ℕ × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure ν]
(m : ℕ)
:
Used by
InformationTheory.Shannon.BroadcastChannel.lintegral_mutualInfo_condDistrib_le_uvQuantizeSlack
source{α : Type u}
{β₁ : Type u_1}
{β₂ : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
(ν : MeasureTheory.Measure (ℕ × ℕ × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure ν]
(m : ℕ)
:
∫⁻ (t : ULift.{u, 0} (Fin (m + 1))), mutualInfo ((ProbabilityTheory.condDistrib id (fun (q : ℕ × ℕ × α × β₁ × β₂) => uvQuantize m q.1) ν) t)
(fun (q : ℕ × ℕ × α × β₁ × β₂) => q.1) fun (q : ℕ × ℕ × α × β₁ × β₂) =>
q.2.2.2.2 ∂MeasureTheory.Measure.map (fun (q : ℕ × ℕ × α × β₁ × β₂) => uvQuantize m q.1) ν ≤ uvQuantizeSlack ν m
Used by
InformationTheory.Shannon.BroadcastChannel.mutualInfo_le_mutualInfo_uvQuantize_add_slack
source{α : Type u}
{β₁ : Type u_1}
{β₂ : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
(ν : MeasureTheory.Measure (ℕ × ℕ × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure ν]
(m : ℕ)
:
Used by
The truncation estimates at the level of the slots #
InformationTheory.Shannon.BroadcastChannel.uvInfo₂_le_uvQuantizeLaw_add_slack
source{α : Type u}
{β₁ : Type u_1}
{β₂ : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
(ν : MeasureTheory.Measure (ℕ × ℕ × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure ν]
(m : ℕ)
:
Used by
InformationTheory.Shannon.BroadcastChannel.uvInfoSum₂_le_uvQuantizeLaw_add_slack
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]
{ν : MeasureTheory.Measure (ℕ × ℕ × α × β₁ × β₂)}
[MeasureTheory.IsProbabilityMeasure ν]
(h : IsUVChannelLaw W ν)
(m : ℕ)
:
Used by
InformationTheory.Shannon.BroadcastChannel.tendsto_uvQuantizeSlack
source{α : Type u}
{β₁ : Type u_1}
{β₂ : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β₁]
[Fintype β₂]
[MeasurableSpace β₂]
(ν : MeasureTheory.Measure (ℕ × ℕ × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure ν]
: