InformationTheory.Shannon.BroadcastChannel.Superposition.FullSupport
Broadcast channel — perturbing an achievability pair to full support #
The superposition inner bound is a union over the pairs whose cloud law and satellite kernel give
every letter positive mass, whereas the pair read off a channel law need not: the law is free to
ignore part of the auxiliary alphabet or part of the input alphabet. Mixing the law with the one
whose auxiliary and input letter are uniform and independent repairs both defects at once, because
the mixture dominates a positive multiple of the uniform law on every singleton of the (U, X)
marginal, and both the cloud law and the satellite kernel are read off exactly that marginal.
The mixture is carried by the auxiliary Bool × U, whose first component records which branch was
taken, so the two information slots of the mixed law are controlled by the slots of the original
one. Forgetting the tag coarsens the conditioner of the satellite slot, which can only increase
it, while the receiver-2 corner pays the entropy of the tag. That penalty is additive rather than
multiplicative, and it has to be: the corner of a mixture is not bounded below by any multiple of
the corner of the branch it keeps. Both losses vanish with the mixing weight, so a rate pair
dominated by the informations of an arbitrary pair is dominated, up to any positive slack, by the
informations of a full-support pair.
Main definitions #
uvUniformLaw W v₀— the channel law whose auxiliary and input letter are uniform and independent, the second auxiliary being frozen atv₀.uvPerturbLaw W ν v₀ lam— the channel law mixed with the uniform one with weightlam.uvLawOfPair W pU K— the five-tuple law of an achievability pair.
Main statements #
exists_fullSupport_bcInfo_ge— a rate pair dominated by the two informations of an achievability pair is dominated, up to any positive slack, by those of a full-support pair.exists_fullSupport_bcInfo_ge_of_isUVChannelLaw— the same statement, with the rate pair dominated by the two slots of a channel law.exists_fullSupport_bcInfo_ge_of_lessNoisy_of_isUVChannelLaw— over a less noisy channel, a rate pair satisfying the three UV outer inequalities of a channel law is dominated, up to any positive slack, by the two informations of a full-support pair.sub_mem_bcSuperpositionRegionNoSumRate_of_lessNoisy_of_isUVChannelLaw— that shifted rate pair lies in the superposition inner bound.
Full support of the achievability pair read off a law #
InformationTheory.Shannon.BroadcastChannel.uvSatelliteKernel_real_singleton_pos
source{α : Type u_1}
[MeasurableSpace α]
[StandardBorelSpace α]
[Nonempty α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{U : Type u_4}
[MeasurableSpace U]
[MeasurableSingletonClass U]
{V : Type u_5}
[MeasurableSpace V]
(μ : MeasureTheory.Measure (U × V × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure μ]
(hpos : ∀ (u : U) (a : α), 0 < (MeasureTheory.Measure.map (fun (q : U × V × α × β₁ × β₂) => (q.1, q.2.2.1)) μ) {(u, a)})
(u : U)
(a : α)
:
Used by
InformationTheory.Shannon.BroadcastChannel.uvCloudLaw_real_singleton_pos
source{α : Type u_1}
[MeasurableSpace α]
[StandardBorelSpace α]
[Nonempty α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{U : Type u_4}
[MeasurableSpace U]
[MeasurableSingletonClass U]
{V : Type u_5}
[MeasurableSpace V]
(μ : MeasureTheory.Measure (U × V × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure μ]
(hpos : ∀ (u : U) (a : α), 0 < (MeasureTheory.Measure.map (fun (q : U × V × α × β₁ × β₂) => (q.1, q.2.2.1)) μ) {(u, a)})
(u : U)
:
Used by
The perturbed law #
InformationTheory.Shannon.BroadcastChannel.uvUniformLaw
source{α : Type u_1}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{U : Type u_4}
[Fintype U]
[Nonempty U]
[MeasurableSpace U]
{V : Type u_5}
[MeasurableSpace V]
(W : BCChannel α β₁ β₂)
(v₀ : V)
:
MeasureTheory.Measure (U × V × α × β₁ × β₂)
The channel law whose auxiliary and input letter are uniform and independent of each other,
the second auxiliary being frozen at v₀.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.uvUniformLaw_isProbabilityMeasure
source{α : Type u_1}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{U : Type u_4}
[Fintype U]
[Nonempty U]
[MeasurableSpace U]
{V : Type u_5}
[MeasurableSpace V]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(v₀ : V)
:
Used by
InformationTheory.Shannon.BroadcastChannel.uvUniformLaw_isUVChannelLaw
source{α : Type u_1}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{U : Type u_4}
[Fintype U]
[Nonempty U]
[MeasurableSpace U]
{V : Type u_5}
[MeasurableSpace V]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(v₀ : V)
:
IsUVChannelLaw W (uvUniformLaw W v₀)
Used by
InformationTheory.Shannon.BroadcastChannel.uvPerturbLaw
source{α : Type u_1}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{U : Type u_4}
[Fintype U]
[Nonempty U]
[MeasurableSpace U]
{V : Type u_5}
[MeasurableSpace V]
(W : BCChannel α β₁ β₂)
(ν : MeasureTheory.Measure (U × V × α × β₁ × β₂))
(v₀ : V)
(lam : ENNReal)
:
MeasureTheory.Measure (U × V × α × β₁ × β₂)
The channel law perturbed toward the uniform one, clamped so that it is a probability measure for every weight.
Equations
- InformationTheory.Shannon.BroadcastChannel.uvPerturbLaw W ν v₀ lam = min lam 1 • ν + (1 - lam) • InformationTheory.Shannon.BroadcastChannel.uvUniformLaw W v₀
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.uvPerturbLaw_isProbabilityMeasure
source{α : Type u_1}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{U : Type u_4}
[Fintype U]
[Nonempty U]
[MeasurableSpace U]
{V : Type u_5}
[MeasurableSpace V]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(ν : MeasureTheory.Measure (U × V × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure ν]
(v₀ : V)
(lam : ENNReal)
:
MeasureTheory.IsProbabilityMeasure (uvPerturbLaw W ν v₀ lam)
Used by
InformationTheory.Shannon.BroadcastChannel.uvPerturbLaw_isUVChannelLaw
source{α : Type u_1}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{U : Type u_4}
[Fintype U]
[Nonempty U]
[MeasurableSpace U]
{V : Type u_5}
[MeasurableSpace V]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
{ν : MeasureTheory.Measure (U × V × α × β₁ × β₂)}
[MeasureTheory.IsProbabilityMeasure ν]
(h : IsUVChannelLaw W ν)
(v₀ : V)
(lam : ENNReal)
:
IsUVChannelLaw W (uvPerturbLaw W ν v₀ lam)
Used by
InformationTheory.Shannon.BroadcastChannel.uvUniformLaw_map_aux_input_pos
source{α : Type u_1}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{U : Type u_4}
[Fintype U]
[Nonempty U]
[MeasurableSpace U]
{V : Type u_5}
[MeasurableSpace V]
[MeasurableSingletonClass α]
[MeasurableSingletonClass U]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(v₀ : V)
(u : U)
(a : α)
:
Used by
InformationTheory.Shannon.BroadcastChannel.uvPerturbLaw_map_aux_input_pos
source{α : Type u_1}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{U : Type u_4}
[Fintype U]
[Nonempty U]
[MeasurableSpace U]
{V : Type u_5}
[MeasurableSpace V]
[MeasurableSingletonClass α]
[MeasurableSingletonClass U]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(ν : MeasureTheory.Measure (U × V × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure ν]
(v₀ : V)
{lam : ENNReal}
(hlam : lam < 1)
(u : U)
(a : α)
:
Used by
Forgetting the tag #
InformationTheory.Shannon.BroadcastChannel.condMutualInfo_le_condMutualInfo_of_isUVChannelLaw_of_map_forget
source{α : Type u_1}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[StandardBorelSpace α]
{β₁ : Type u_2}
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[StandardBorelSpace β₁]
{β₂ : Type u_3}
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
{U : Type u_4}
[MeasurableSpace U]
[StandardBorelSpace U]
[Nonempty U]
{V : Type u_5}
[MeasurableSpace V]
[StandardBorelSpace V]
[Nonempty V]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(μ : MeasureTheory.Measure ((Bool × U) × V × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure μ]
(h : IsUVChannelLaw W μ)
(ρ : MeasureTheory.Measure (U × V × α × β₁ × β₂))
[MeasureTheory.IsFiniteMeasure ρ]
(hρ : ρ = MeasureTheory.Measure.map (uvRelabel Prod.snd id) μ)
:
(condMutualInfo μ (fun (q : (Bool × U) × V × α × β₁ × β₂) => q.2.2.1)
(fun (q : (Bool × U) × V × α × β₁ × β₂) => q.2.2.2.1) fun (q : (Bool × U) × V × α × β₁ × β₂) => q.1) ≤ condMutualInfo ρ (fun (q : U × V × α × β₁ × β₂) => q.2.2.1) (fun (q : U × V × α × β₁ × β₂) => q.2.2.2.1)
fun (q : U × V × α × β₁ × β₂) => q.1
Used by
InformationTheory.Shannon.BroadcastChannel.uvInfo₂_le_uvInfo₂_map_forget_add_entropy
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
[StandardBorelSpace β₂]
{U : Type u_4}
[Fintype U]
[MeasurableSpace U]
[StandardBorelSpace U]
[Nonempty U]
[MeasurableSingletonClass U]
{V : Type u_5}
[MeasurableSpace V]
(μ : MeasureTheory.Measure ((Bool × U) × V × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure μ]
:
Used by
The two slots of the perturbed law #
InformationTheory.Shannon.BroadcastChannel.mul_condMutualInfo_le_condMutualInfo_uvPerturbLaw
source{α : Type u_1}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[StandardBorelSpace α]
{β₁ : Type u_2}
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[StandardBorelSpace β₁]
{β₂ : Type u_3}
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
{U : Type u_4}
[Fintype U]
[MeasurableSpace U]
[StandardBorelSpace U]
[Nonempty U]
{V : Type u_5}
[MeasurableSpace V]
[StandardBorelSpace V]
[Nonempty V]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
{ν : MeasureTheory.Measure (U × V × α × β₁ × β₂)}
[MeasureTheory.IsProbabilityMeasure ν]
(h : IsUVChannelLaw W ν)
(v₀ : V)
{lam : ENNReal}
(hlam : lam ≤ 1)
:
(lam * condMutualInfo ν (fun (q : U × V × α × β₁ × β₂) => q.2.2.1) (fun (q : U × V × α × β₁ × β₂) => q.2.2.2.1)
fun (q : U × V × α × β₁ × β₂) => q.1) ≤ condMutualInfo (uvPerturbLaw W ν v₀ lam) (fun (q : U × V × α × β₁ × β₂) => q.2.2.1)
(fun (q : U × V × α × β₁ × β₂) => q.2.2.2.1) fun (q : U × V × α × β₁ × β₂) => q.1
Used by
InformationTheory.Shannon.BroadcastChannel.mul_uvInfo₂_sub_binEntropy_le_uvInfo₂_uvPerturbLaw
source{α : Type u_1}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
[StandardBorelSpace β₂]
{U : Type u_4}
[Fintype U]
[MeasurableSpace U]
[StandardBorelSpace U]
[Nonempty U]
[MeasurableSingletonClass U]
{V : Type u_5}
[MeasurableSpace V]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
{ν : MeasureTheory.Measure (U × V × α × β₁ × β₂)}
[MeasureTheory.IsProbabilityMeasure ν]
(v₀ : V)
{lam : ENNReal}
(hlam : lam ≤ 1)
:
Used by
The full-support pair of a channel law #
InformationTheory.Shannon.BroadcastChannel.exists_fullSupport_bcInfo_ge_of_isUVChannelLaw
source{α : Type u}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[StandardBorelSpace α]
{β₁ : Type u_1}
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[StandardBorelSpace β₁]
{β₂ : Type u_2}
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
[StandardBorelSpace β₂]
{U : Type u}
[Fintype U]
[Nonempty U]
[MeasurableSpace U]
[MeasurableSingletonClass U]
[StandardBorelSpace U]
{V : Type u_3}
[MeasurableSpace V]
[StandardBorelSpace V]
[Nonempty V]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
{ν : MeasureTheory.Measure (U × V × α × β₁ × β₂)}
[MeasureTheory.IsProbabilityMeasure ν]
(h : IsUVChannelLaw W ν)
{R₁ R₂ δ : ℝ}
(hδ : 0 < δ)
(h₁ :
R₁ ≤ (condMutualInfo ν (fun (q : U × V × α × β₁ × β₂) => q.2.2.1) (fun (q : U × V × α × β₁ × β₂) => q.2.2.2.1)
fun (q : U × V × α × β₁ × β₂) => q.1).toReal)
(h₂ : R₂ ≤ (uvInfo₂ ν).toReal)
:
∃ (pU : MeasureTheory.Measure U) (_ : MeasureTheory.IsProbabilityMeasure pU) (_ : ∀ (u : U), 0 < pU.real {u}) (K :
ProbabilityTheory.Kernel U α) (_ : ProbabilityTheory.IsMarkovKernel K) (_ : ∀ (u : U) (a : α), 0 < (K u).real {a}),
R₁ - δ ≤ bcInfo₁ pU K W ∧ R₂ - δ ≤ bcInfo₂ pU K W
Used by
The pair-level statement #
InformationTheory.Shannon.BroadcastChannel.uvLawOfPair
source{α : Type u}
[MeasurableSpace α]
{β₁ : Type u_1}
[MeasurableSpace β₁]
{β₂ : Type u_2}
[MeasurableSpace β₂]
{U : Type u}
[MeasurableSpace U]
(W : BCChannel α β₁ β₂)
(pU : MeasureTheory.Measure U)
(K : ProbabilityTheory.Kernel U α)
:
MeasureTheory.Measure (U × U × α × β₁ × β₂)
The five-tuple law of an achievability pair, with the second auxiliary a copy of the first, so that it carries no information beyond it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.uvLawOfPair_isProbabilityMeasure
source{α : Type u}
[MeasurableSpace α]
{β₁ : Type u_1}
[MeasurableSpace β₁]
{β₂ : Type u_2}
[MeasurableSpace β₂]
{U : Type u}
[MeasurableSpace U]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(pU : MeasureTheory.Measure U)
[MeasureTheory.IsProbabilityMeasure pU]
(K : ProbabilityTheory.Kernel U α)
[ProbabilityTheory.IsMarkovKernel K]
:
Used by
InformationTheory.Shannon.BroadcastChannel.exists_fullSupport_bcInfo_ge
source{α : Type u}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[StandardBorelSpace α]
{β₁ : Type u_1}
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[StandardBorelSpace β₁]
{β₂ : Type u_2}
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
[StandardBorelSpace β₂]
{U : Type u}
[Fintype U]
[Nonempty U]
[MeasurableSpace U]
[MeasurableSingletonClass U]
[StandardBorelSpace U]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(pU : MeasureTheory.Measure U)
[MeasureTheory.IsProbabilityMeasure pU]
(K : ProbabilityTheory.Kernel U α)
[ProbabilityTheory.IsMarkovKernel K]
{R₁ R₂ δ : ℝ}
(hδ : 0 < δ)
(h₁ : R₁ ≤ bcInfo₁ pU K W)
(h₂ : R₂ ≤ bcInfo₂ pU K W)
:
∃ (pU' : MeasureTheory.Measure U) (_ : MeasureTheory.IsProbabilityMeasure pU') (_ : ∀ (u : U), 0 < pU'.real {u}) (K' :
ProbabilityTheory.Kernel U α) (_ : ProbabilityTheory.IsMarkovKernel K') (_ : ∀ (u : U) (a : α), 0 < (K' u).real {a}),
R₁ - δ ≤ bcInfo₁ pU' K' W ∧ R₂ - δ ≤ bcInfo₂ pU' K' W
A rate pair dominated by the two informations of an achievability pair is dominated, up to any positive slack, by the two informations of a pair giving every letter positive mass.
Used by
Composition with time sharing #
InformationTheory.Shannon.BroadcastChannel.exists_fullSupport_bcInfo_ge_of_lessNoisy_of_isUVChannelLaw
source{α : Type u}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[StandardBorelSpace α]
{β₁ : Type u_1}
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[StandardBorelSpace β₁]
{β₂ : Type u_2}
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
[StandardBorelSpace β₂]
{V : Type u_3}
[MeasurableSpace V]
[StandardBorelSpace V]
[Nonempty V]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(hln : IsBCLessNoisy W)
{m : ℕ}
{ν : MeasureTheory.Measure (Marton.bcAuxAlphabet m × V × α × β₁ × β₂)}
[MeasureTheory.IsProbabilityMeasure ν]
(h : IsUVChannelLaw W ν)
{R₁ R₂ δ : ℝ}
(hδ : 0 < δ)
(h₁ : R₁ ≤ (uvInfo₁ ν).toReal)
(h₂ : R₂ ≤ (uvInfo₂ ν).toReal)
(hsum : R₁ + R₂ ≤ (uvInfoSum₂ ν).toReal)
:
∃ (k : ℕ) (pU : MeasureTheory.Measure (Marton.bcAuxAlphabet k)) (_ : MeasureTheory.IsProbabilityMeasure pU) (_ :
∀ (x : Marton.bcAuxAlphabet k), 0 < pU.real {x}) (K : ProbabilityTheory.Kernel (Marton.bcAuxAlphabet k) α) (_ :
ProbabilityTheory.IsMarkovKernel K) (_ : ∀ (x : Marton.bcAuxAlphabet k) (a : α), 0 < (K x).real {a}),
R₁ - δ ≤ bcInfo₁ pU K W ∧ R₂ - δ ≤ bcInfo₂ pU K W
Over a less noisy channel, a rate pair satisfying the three UV outer inequalities of a channel law is dominated, up to any positive slack, by the two informations of an achievability pair whose cloud law and satellite kernel give every letter positive mass.
Used by
InformationTheory.Shannon.BroadcastChannel.sub_mem_bcSuperpositionRegionNoSumRate_of_lessNoisy_of_isUVChannelLaw
source{α : Type u}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[StandardBorelSpace α]
{β₁ : Type u_1}
[Fintype β₁]
[Nonempty β₁]
[MeasurableSpace β₁]
[MeasurableSingletonClass β₁]
[StandardBorelSpace β₁]
{β₂ : Type u_2}
[Fintype β₂]
[Nonempty β₂]
[MeasurableSpace β₂]
[MeasurableSingletonClass β₂]
[StandardBorelSpace β₂]
{V : Type u_3}
[MeasurableSpace V]
[StandardBorelSpace V]
[Nonempty V]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(hln : IsBCLessNoisy W)
{m : ℕ}
{ν : MeasureTheory.Measure (Marton.bcAuxAlphabet m × V × α × β₁ × β₂)}
[MeasureTheory.IsProbabilityMeasure ν]
(h : IsUVChannelLaw W ν)
{R₁ R₂ δ : ℝ}
(hδ : 0 < δ)
(h₁ : R₁ ≤ (uvInfo₁ ν).toReal)
(h₂ : R₂ ≤ (uvInfo₂ ν).toReal)
(hsum : R₁ + R₂ ≤ (uvInfoSum₂ ν).toReal)
: