InformationTheory.Shannon.SlepianWolf.FullRateRegion.PairBound
The strict swError_EXY expectation bound under random binning #
The "both coordinates differ" sub-event swError_EXY_strict admits the bound
|JTS| / (M_X · M_Y) via pair-binning collision (1/M_X · 1/M_Y) summed over the
joint typical set, which with jointlyTypicalSet_card_le gives the target
exp(n · (H(X,Y) + ε)) / (M_X · M_Y). The original swError_EXY splits into three
sub-cases by (p.1 = Xⁿ ?, p.2 = Yⁿ ?); the two "loose" cases are absorbed into
swError_EX / swError_EY via swError_EXY_subset_union.
InformationTheory.Shannon.ChannelCoding.swError_EXY_strict
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[MeasurableSpace α]
{β : Type u_3}
[Fintype β]
[MeasurableSpace β]
(μ : MeasureTheory.Measure Ω)
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
(n : ℕ)
{M_X M_Y : ℕ}
(ε : ℝ)
(f_X : (Fin n → α) → Fin M_X)
(f_Y : (Fin n → β) → Fin M_Y)
:
Set Ω
The "both coordinates differ" sub-event of swError_EXY.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Used by
InformationTheory.Shannon.ChannelCoding.measureReal_swError_EXY_strict_le_one
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
{β : Type u_3}
[Fintype β]
[Nonempty β]
[MeasurableSpace β]
[MeasurableSingletonClass β]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
{n M_X M_Y : ℕ}
(ε : ℝ)
(f_X : (Fin n → α) → Fin M_X)
(f_Y : (Fin n → β) → Fin M_Y)
:
Used by
InformationTheory.Shannon.ChannelCoding.swError_EXY_subset_union
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
{β : Type u_3}
[Fintype β]
[Nonempty β]
[MeasurableSpace β]
[MeasurableSingletonClass β]
(μ : MeasureTheory.Measure Ω)
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
{n M_X M_Y : ℕ}
(ε : ℝ)
(f_X : (Fin n → α) → Fin M_X)
(f_Y : (Fin n → β) → Fin M_Y)
:
swError_EXY μ Xs Ys n ε f_X f_Y ⊆ swError_EX μ Xs Ys n ε f_X ∪ swError_EY μ Xs Ys n ε f_Y ∪ swError_EXY_strict μ Xs Ys n ε f_X f_Y
The full swError_EXY event is contained in the union of the two single-axis
events swError_EX, swError_EY and the strict swError_EXY_strict. The loose
cases (only one coordinate of the alias p agrees with the truth) are absorbed
into E_X or E_Y respectively.
Used by
The swError_EXY_strict expectation bound #
The expected μ-mass of the strict E_{XY} error event (both alias coordinates
differ from the truth) over the product random binning hash
(f_X, f_Y) ∼ (binningMeasure α n M_X) × (binningMeasure β n M_Y) is bounded by
exp(n · (H(X, Y) + ε)) / (M_X · M_Y), the joint typical set's cardinality bound
divided by the product bin count. The proof Fubini-swaps BP := B_X × B_Y and μ,
applies binning_pair_alias_expectation_le_aux per ω, and closes with
jointlyTypicalSet_card_le.
InformationTheory.Shannon.ChannelCoding.swError_EXY_strict_expectation_le
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
{β : Type u_3}
[Fintype β]
[Nonempty β]
[MeasurableSpace β]
[MeasurableSingletonClass β]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
(hXs : ∀ (i : ℕ), Measurable (Xs i))
(hYs : ∀ (i : ℕ), Measurable (Ys i))
(hposZ : ∀ (p : α × β), 0 < (MeasureTheory.Measure.map (jointSequence Xs Ys 0) μ).real {p})
{n M_X M_Y : ℕ}
[NeZero M_X]
[NeZero M_Y]
{ε : ℝ}
(hε : 0 < ε)
:
Used by
Pigeonhole and finalize (Cover–Thomas) #
Combines the four-event decomposition with the per-term binning bounds, takes a total
bound over the binning expectation, extracts a deterministic encoder pair by
pigeonhole, and derives error probability → 0 under the rate conditions
R_X > H(Y|X), R_Y > H(X|Y), R_X + R_Y > H(X, Y).
entropy_joint_sub_marginal_eq_condEntropy— the bridgeH(X,Y) - H(X) = H(Y|X).swErrorProb_total_expectation_le— the total binning-expectation bound.exists_pair_le_of_binning_integral_le— pigeonhole extraction.slepian_wolf_full_rate_region_achievability— rate region achievability.
InformationTheory.Shannon.ChannelCoding.swErrorProb_le_one
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
{β : Type u_3}
[Fintype β]
[Nonempty β]
[MeasurableSpace β]
[MeasurableSingletonClass β]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
{n M_X M_Y : ℕ}
(ε : ℝ)
(f_X : (Fin n → α) → Fin M_X)
(f_Y : (Fin n → β) → Fin M_Y)
:
Used by
InformationTheory.Shannon.ChannelCoding.integrable_measureReal_swError_EXY_strict_inner
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
{β : Type u_3}
[Fintype β]
[Nonempty β]
[MeasurableSpace β]
[MeasurableSingletonClass β]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
{n M_X M_Y : ℕ}
[NeZero M_Y]
(ε : ℝ)
(f_X : (Fin n → α) → Fin M_X)
:
MeasureTheory.Integrable (fun (f_Y : (Fin n → β) → Fin M_Y) => μ.real (swError_EXY_strict μ Xs Ys n ε f_X f_Y))
(binningMeasure β n M_Y)
Used by
InformationTheory.Shannon.ChannelCoding.integrable_measureReal_swError_EXY_strict_outer
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
{β : Type u_3}
[Fintype β]
[Nonempty β]
[MeasurableSpace β]
[MeasurableSingletonClass β]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
{n M_X M_Y : ℕ}
[NeZero M_X]
[NeZero M_Y]
(ε : ℝ)
:
MeasureTheory.Integrable
(fun (f_X : (Fin n → α) → Fin M_X) =>
∫ (f_Y : (Fin n → β) → Fin M_Y), μ.real (swError_EXY_strict μ Xs Ys n ε f_X f_Y) ∂binningMeasure β n M_Y)
(binningMeasure α n M_X)
Used by
InformationTheory.Shannon.ChannelCoding.swErrorProb_inner_integral_le
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
{β : Type u_3}
[Fintype β]
[Nonempty β]
[MeasurableSpace β]
[MeasurableSingletonClass β]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
{n M_X M_Y : ℕ}
[NeZero M_Y]
(ε : ℝ)
(f_X : (Fin n → α) → Fin M_X)
(h_pointwise :
∀ (f_Y : (Fin n → β) → Fin M_Y),
swErrorProb μ (jointRV Xs n) (jointRV Ys n) f_X f_Y (swJointTypicalDecoder μ Xs Ys ε f_X f_Y) ≤ μ.real (swError_E0 μ Xs Ys n ε) + 2 * μ.real (swError_EX μ Xs Ys n ε f_X) + 2 * μ.real (swError_EY μ Xs Ys n ε f_Y) + μ.real (swError_EXY_strict μ Xs Ys n ε f_X f_Y))
(hInt_swErr_inner :
MeasureTheory.Integrable
(fun (f_Y : (Fin n → β) → Fin M_Y) =>
swErrorProb μ (jointRV Xs n) (jointRV Ys n) f_X f_Y (swJointTypicalDecoder μ Xs Ys ε f_X f_Y))
(binningMeasure β n M_Y))
(hInt_EY :
MeasureTheory.Integrable (fun (f_Y : (Fin n → β) → Fin M_Y) => μ.real (swError_EY μ Xs Ys n ε f_Y))
(binningMeasure β n M_Y))
(hInt_EXY_strict_inner :
MeasureTheory.Integrable (fun (f_Y : (Fin n → β) → Fin M_Y) => μ.real (swError_EXY_strict μ Xs Ys n ε f_X f_Y))
(binningMeasure β n M_Y))
:
∫ (f_Y : (Fin n → β) → Fin M_Y), swErrorProb μ (jointRV Xs n) (jointRV Ys n) f_X f_Y
(swJointTypicalDecoder μ Xs Ys ε f_X f_Y) ∂binningMeasure β n M_Y ≤ μ.real (swError_E0 μ Xs Ys n ε) + 2 * μ.real (swError_EX μ Xs Ys n ε f_X) + 2 * ∫ (f_Y : (Fin n → β) → Fin M_Y), μ.real (swError_EY μ Xs Ys n ε f_Y) ∂binningMeasure β n M_Y + ∫ (f_Y : (Fin n → β) → Fin M_Y), μ.real (swError_EXY_strict μ Xs Ys n ε f_X f_Y) ∂binningMeasure β n M_Y
Used by
InformationTheory.Shannon.ChannelCoding.integrable_swError_outer_bound
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
{β : Type u_3}
[Fintype β]
[Nonempty β]
[MeasurableSpace β]
[MeasurableSingletonClass β]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
{n M_X M_Y : ℕ}
[NeZero M_X]
[NeZero M_Y]
(ε : ℝ)
(hInt_EX :
MeasureTheory.Integrable (fun (f_X : (Fin n → α) → Fin M_X) => μ.real (swError_EX μ Xs Ys n ε f_X))
(binningMeasure α n M_X))
(hInt_EXY_strict_outer :
MeasureTheory.Integrable
(fun (f_X : (Fin n → α) → Fin M_X) =>
∫ (f_Y : (Fin n → β) → Fin M_Y), μ.real (swError_EXY_strict μ Xs Ys n ε f_X f_Y) ∂binningMeasure β n M_Y)
(binningMeasure α n M_X))
:
MeasureTheory.Integrable
(fun (f_X : (Fin n → α) → Fin M_X) =>
μ.real (swError_E0 μ Xs Ys n ε) + 2 * μ.real (swError_EX μ Xs Ys n ε f_X) + 2 * ∫ (f_Y : (Fin n → β) → Fin M_Y), μ.real (swError_EY μ Xs Ys n ε f_Y) ∂binningMeasure β n M_Y + ∫ (f_Y : (Fin n → β) → Fin M_Y), μ.real (swError_EXY_strict μ Xs Ys n ε f_X f_Y) ∂binningMeasure β n M_Y)
(binningMeasure α n M_X)
Used by
InformationTheory.Shannon.ChannelCoding.integral_swError_outer_split
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
{β : Type u_3}
[Fintype β]
[Nonempty β]
[MeasurableSpace β]
[MeasurableSingletonClass β]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
{n M_X M_Y : ℕ}
[NeZero M_X]
[NeZero M_Y]
(ε : ℝ)
(hInt_EX :
MeasureTheory.Integrable (fun (f_X : (Fin n → α) → Fin M_X) => μ.real (swError_EX μ Xs Ys n ε f_X))
(binningMeasure α n M_X))
(hInt_EXY_strict_outer :
MeasureTheory.Integrable
(fun (f_X : (Fin n → α) → Fin M_X) =>
∫ (f_Y : (Fin n → β) → Fin M_Y), μ.real (swError_EXY_strict μ Xs Ys n ε f_X f_Y) ∂binningMeasure β n M_Y)
(binningMeasure α n M_X))
:
∫ (f_X : (Fin n → α) → Fin M_X), μ.real (swError_E0 μ Xs Ys n ε) + 2 * μ.real (swError_EX μ Xs Ys n ε f_X) + 2 * ∫ (f_Y : (Fin n → β) → Fin M_Y), μ.real (swError_EY μ Xs Ys n ε f_Y) ∂binningMeasure β n M_Y + ∫ (f_Y : (Fin n → β) → Fin M_Y), μ.real (swError_EXY_strict μ Xs Ys n ε f_X f_Y) ∂binningMeasure β n M_Y ∂binningMeasure α n M_X = μ.real (swError_E0 μ Xs Ys n ε) + 2 * ∫ (f_X : (Fin n → α) → Fin M_X), μ.real (swError_EX μ Xs Ys n ε f_X) ∂binningMeasure α n M_X + 2 * ∫ (f_Y : (Fin n → β) → Fin M_Y), μ.real (swError_EY μ Xs Ys n ε f_Y) ∂binningMeasure β n M_Y + ∫ (f_X : (Fin n → α) → Fin M_X), ∫ (f_Y : (Fin n → β) → Fin M_Y), μ.real (swError_EXY_strict μ Xs Ys n ε f_X f_Y) ∂binningMeasure β n M_Y ∂binningMeasure α n M_X
Used by
Exponential squeeze with rate parametrization #
For M_n := codebookSize R n = ⌈exp(n R)⌉, the inverse M_n⁻¹ ≤ exp(-n R), so each
expectation bound exp(n c) · M_n⁻¹ is ≤ exp(n (c - R)), which tends to 0
whenever c < R. This turns the per-term expectation bounds into Tendsto (𝓝 0).
Slepian–Wolf full rate region achievability #
Assembles the error decomposition, the per-term binning bounds, the total binning
expectation, the pigeonhole extraction, and the exponential squeeze into the
achievability of the full Slepian–Wolf rate region: for any rates strictly above the
conditional entropies H(X|Y), H(Y|X) and the joint entropy H(X,Y), there is a
sequence of binning encoders and joint typicality decoders whose error probability
tends to 0.
References #
- T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.
InformationTheory.Shannon.ChannelCoding.slepian_wolf_full_rate_region_achievability
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
{β : Type u_3}
[Fintype β]
[Nonempty β]
[MeasurableSpace β]
[MeasurableSingletonClass β]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
(hXs : ∀ (i : ℕ), Measurable (Xs i))
(hYs : ∀ (i : ℕ), Measurable (Ys i))
(hindepX_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ)
(hidentX : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ)
(hindepY_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Ys i) μ)
(hidentY : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Ys i) (Ys 0) μ μ)
(hindepZ_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => jointSequence Xs Ys i) μ)
(hidentZ : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (jointSequence Xs Ys i) (jointSequence Xs Ys 0) μ μ)
(hposX : ∀ (x : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {x})
(hposY : ∀ (y : β), 0 < (MeasureTheory.Measure.map (Ys 0) μ).real {y})
(hposZ : ∀ (p : α × β), 0 < (MeasureTheory.Measure.map (jointSequence Xs Ys 0) μ).real {p})
{R_X R_Y : ℝ}
(hRX : MeasureFano.condEntropy μ (Xs 0) (Ys 0) < R_X)
(hRY : MeasureFano.condEntropy μ (Ys 0) (Xs 0) < R_Y)
(hRXY : entropy μ (jointSequence Xs Ys 0) < R_X + R_Y)
:
∃ (M_X : ℕ → ℕ) (M_Y : ℕ → ℕ),
(∀ (n : ℕ), 0 < M_X n) ∧ (∀ (n : ℕ), 0 < M_Y n) ∧ ∃ (f_X : (n : ℕ) → (Fin n → α) → Fin (M_X n)) (f_Y : (n : ℕ) → (Fin n → β) → Fin (M_Y n)) (d :
(n : ℕ) → Fin (M_X n) × Fin (M_Y n) → (Fin n → α) × (Fin n → β)),
Filter.Tendsto (fun (n : ℕ) => Real.log ↑(M_X n) / ↑n) Filter.atTop (nhds R_X) ∧ Filter.Tendsto (fun (n : ℕ) => Real.log ↑(M_Y n) / ↑n) Filter.atTop (nhds R_Y) ∧ Filter.Tendsto (fun (n : ℕ) => swErrorProb μ (jointRV Xs n) (jointRV Ys n) (f_X n) (f_Y n) (d n))
Filter.atTop (nhds 0)
Slepian–Wolf theorem (full rate region achievability): for an
i.i.d. source (Xⁿ, Yⁿ) with full support, any rate pair (R_X, R_Y) with
R_X > H(X|Y), R_Y > H(Y|X), R_X + R_Y > H(X,Y) is achievable: there are
codebook sizes M_X, M_Y with the required asymptotic rates and encoders/decoders
whose error probability → 0.
@audit:ok