InformationTheory.Shannon.RateDistortion.AchievabilityStrongTypicality.SupportingBounds
Rate-distortion achievability (strong-typicality variant) — supporting bounds #
The per-source match-probability and encoder-failure bounds, the
generic-encoder distortion decomposition, the strong lossy-code bundle, the
witness-form and ambient-measure wrappers, codebookAvgFailureStrong, and the
rdAmbient entropy / block-law bridges.
Step A — Per-source-typical match probability lower bound #
InformationTheory.Shannon.per_source_typical_match_prob_strong_ge
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSingletonClass α]
[Fintype β]
[DecidableEq β]
[Nonempty β]
[MeasurableSingletonClass β]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
(hXs : ∀ (i : ℕ), Measurable (Xs i))
(hYs : ∀ (i : ℕ), Measurable (Ys i))
(hindep_Z_pair :
Pairwise fun (i j : ℕ) =>
ProbabilityTheory.IndepFun (ChannelCoding.jointSequence Xs Ys i) (ChannelCoding.jointSequence Xs Ys j) μ)
(hident_Z :
∀ (i : ℕ),
ProbabilityTheory.IdentDistrib (ChannelCoding.jointSequence Xs Ys i) (ChannelCoding.jointSequence Xs Ys 0) μ μ)
(hposZ : ∀ (p : α × β), 0 < (MeasureTheory.Measure.map (ChannelCoding.jointSequence Xs Ys 0) μ).real {p})
(hposX : ∀ (a : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {a})
(hposY : ∀ (b : β), 0 < (MeasureTheory.Measure.map (Ys 0) μ).real {b})
(hmarg_X :
MeasureTheory.Measure.map Prod.fst (MeasureTheory.Measure.map (ChannelCoding.jointSequence Xs Ys 0) μ) = MeasureTheory.Measure.map (Xs 0) μ)
(hmarg_Y :
MeasureTheory.Measure.map Prod.snd (MeasureTheory.Measure.map (ChannelCoding.jointSequence Xs Ys 0) μ) = MeasureTheory.Measure.map (Ys 0) μ)
{ε ε_X δ : ℝ}
(hε : 0 < ε)
(hε_X : 0 ≤ ε_X)
(hε_X_lt_ε : ε_X < ε)
(hδ : 0 < δ)
(qZ_min : ℝ)
(hqZ_min_pos : 0 < qZ_min)
(hqZ_min_le : ∀ (p : α × β), qZ_min ≤ (MeasureTheory.Measure.map (ChannelCoding.jointSequence Xs Ys 0) μ).real {p})
(hδ_dominates_kl : 8 * ↑(Fintype.card α) * ↑(Fintype.card β) * ε_X ^ 2 ≤ δ * qZ_min)
:
∃ (N : ℕ),
∀ (n : ℕ),
N ≤ n →
∀ x ∈ stronglyTypicalSet μ Xs n ε_X,
Real.exp
(-↑n * (entropy μ (Xs 0) + entropy μ (Ys 0) - entropy μ (ChannelCoding.jointSequence Xs Ys 0) + (↑(Fintype.card α) * ε_X * logSumAbs μ Ys + ε_X * logSumAbs μ Xs + ε_X * logSumAbs μ (ChannelCoding.jointSequence Xs Ys) + δ))) ≤ (MeasureTheory.Measure.pi fun (x : Fin n) => MeasureTheory.Measure.map (Ys 0) μ).real
{y : Fin n → β | (x, y) ∈ jointStronglyTypicalSet μ Xs Ys n ε}
Step A: repackage conditionalStronglyTypicalSlice_mass_ge for the
random-coding chain. For x X-strongly-typical (eventually in n), the
probability under the Y-product measure that a random y lands in the joint
strong slice at x is bounded below by exp(-n · (H(X) + H(Y) - H(Z) + slack)).
Used by
Step B — Encoder failure probability bound (strong version) #
InformationTheory.Shannon.encoder_strong_failure_prob_le
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSingletonClass α]
[Fintype β]
[DecidableEq β]
[Nonempty β]
[MeasurableSingletonClass β]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
(hXs : ∀ (i : ℕ), Measurable (Xs i))
(hYs : ∀ (i : ℕ), Measurable (Ys i))
(hindep_Z_pair :
Pairwise fun (i j : ℕ) =>
ProbabilityTheory.IndepFun (ChannelCoding.jointSequence Xs Ys i) (ChannelCoding.jointSequence Xs Ys j) μ)
(hident_Z :
∀ (i : ℕ),
ProbabilityTheory.IdentDistrib (ChannelCoding.jointSequence Xs Ys i) (ChannelCoding.jointSequence Xs Ys 0) μ μ)
(hposZ : ∀ (p : α × β), 0 < (MeasureTheory.Measure.map (ChannelCoding.jointSequence Xs Ys 0) μ).real {p})
(hposX : ∀ (a : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {a})
(hposY : ∀ (b : β), 0 < (MeasureTheory.Measure.map (Ys 0) μ).real {b})
(hmarg_X :
MeasureTheory.Measure.map Prod.fst (MeasureTheory.Measure.map (ChannelCoding.jointSequence Xs Ys 0) μ) = MeasureTheory.Measure.map (Xs 0) μ)
(hmarg_Y :
MeasureTheory.Measure.map Prod.snd (MeasureTheory.Measure.map (ChannelCoding.jointSequence Xs Ys 0) μ) = MeasureTheory.Measure.map (Ys 0) μ)
{ε ε_X δ : ℝ}
(hε : 0 < ε)
(hε_X : 0 ≤ ε_X)
(hε_X_lt_ε : ε_X < ε)
(hδ : 0 < δ)
(qZ_min : ℝ)
(hqZ_min_pos : 0 < qZ_min)
(hqZ_min_le : ∀ (p : α × β), qZ_min ≤ (MeasureTheory.Measure.map (ChannelCoding.jointSequence Xs Ys 0) μ).real {p})
(hδ_dominates_kl : 8 * ↑(Fintype.card α) * ↑(Fintype.card β) * ε_X ^ 2 ≤ δ * qZ_min)
:
∃ (N : ℕ),
∀ (n : ℕ),
N ≤ n →
∀ (M : ℕ),
∀ x ∈ stronglyTypicalSet μ Xs n ε_X,
(MeasureTheory.Measure.pi fun (x : Fin M) =>
MeasureTheory.Measure.pi fun (x : Fin n) => MeasureTheory.Measure.map (Ys 0) μ).real
{c : Fin M → Fin n → β | ∀ (m : Fin M), (x, c m) ∉ jointStronglyTypicalSet μ Xs Ys n ε} ≤ Real.exp
(-↑M * Real.exp
(-↑n * (entropy μ (Xs 0) + entropy μ (Ys 0) - entropy μ (ChannelCoding.jointSequence Xs Ys 0) + (↑(Fintype.card α) * ε_X * logSumAbs μ Ys + ε_X * logSumAbs μ Xs + ε_X * logSumAbs μ (ChannelCoding.jointSequence Xs Ys) + δ))))
Step B: For x ∈ stronglyTypicalSet μ Xs n ε_X (eventually in n),
the codebook-averaged probability that no codeword is jointly-strongly-typical
with x is bounded by exp(-M · exp(-n(H(X)+H(Y)-H(Z)+slack))). Strong analogue
of encoder_failure_prob_le_exp_neg_M_avg.
Used by
Generic-encoder distortion decomposition #
InformationTheory.Shannon.source_avg_distortion_le_simpler_generic
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[Fintype α]
[Nonempty α]
[MeasurableSingletonClass α]
[Fintype β]
[Nonempty β]
[MeasurableSingletonClass β]
(μ : MeasureTheory.Measure Ω)
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
(d : DistortionFn α β)
{M n : ℕ}
(ε : ℝ)
{δ : ℝ}
(hδ : 0 ≤ δ)
(c : ChannelCoding.Codebook M n β)
(enc : (Fin n → α) → Fin M)
(P_X : MeasureTheory.Measure (Fin n → α))
[MeasureTheory.IsProbabilityMeasure P_X]
:
Generic-encoder distortion decomposition, the analogue of
source_avg_distortion_le_simpler with the joint-typical encoder replaced by an
arbitrary encoder function.
Used by
Strong lossy-code-of-codebook bundle #
InformationTheory.Shannon.lossyCodeOfCodebookStrong
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[DecidableEq α]
[DecidableEq β]
(μ : MeasureTheory.Measure Ω)
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
{M n : ℕ}
(hM : 0 < M)
(ε : ℝ)
(c : ChannelCoding.Codebook M n β)
:
LossyCode M n α β
Bundle a codebook + strong-JTS lossy encoder into a LossyCode. Strong
analogue of lossyCodeOfCodebook.
Equations
- InformationTheory.Shannon.lossyCodeOfCodebookStrong μ Xs Ys hM ε c = { encoder := InformationTheory.Shannon.jointStronglyTypicalLossyEncoder μ Xs Ys hM ε c, decoder := c }
Instances For
Used by
InformationTheory.Shannon.weighted_avg_bound
source{ι : Type u_4}
[Fintype ι]
(W f g : ι → ℝ)
(a m B : ℝ)
(hW_nn : ∀ (i : ι), 0 ≤ W i)
(hW_sum : ∑ i : ι, W i = 1)
(hm_nn : 0 ≤ m)
(h_per : ∀ (i : ι), f i ≤ a + m * g i)
(h_g : ∑ i : ι, W i * g i ≤ B)
:
Weighted-average bound: if 0 ≤ W with ∑ W = 1, each f i ≤ a + m * g i,
0 ≤ m, and ∑ W · g ≤ B, then ∑ W · f ≤ a + m · B.
Used by
Witness-form rate-distortion achievability (strong-encoder variant) #
The strong-encoder analogue of rate_distortion_achievability_witness_form,
with jointTypicalLossyEncoder replaced by jointStronglyTypicalLossyEncoder.
The argument composes the per-codebook distortion decomposition (the generic
source_avg_distortion_le_simpler_generic), a weighted sum, and pigeonhole.
InformationTheory.Shannon.rate_distortion_achievability_witness_form_strong
source{Ω : Type u_1}
[MeasurableSpace Ω]
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSingletonClass α]
[Fintype β]
[DecidableEq β]
[Nonempty β]
[MeasurableSingletonClass β]
(P_X_pmf : α → ℝ)
(d : DistortionFn α β)
{D : ℝ}
(qStar : α × β → ℝ)
(hqStar_mem : qStar ∈ RDConstraint P_X_pmf d D)
{R : ℝ}
(hI_lt_R : mutualInfoPmf qStar < R)
{ε' : ℝ}
(hε' : 0 < ε')
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : ℕ → Ω → α)
(Ys : ℕ → Ω → β)
(hXs : ∀ (i : ℕ), Measurable (Xs i))
(hYs : ∀ (i : ℕ), Measurable (Ys i))
[MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map (Xs 0) μ)]
[MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map (Ys 0) μ)]
(h_dist_eq : expectedJointDistortion μ (Xs 0) (Ys 0) d = expectedDistortionPmf d qStar)
(ε_join ε_dist δ_typ : ℝ)
(hδ_typ : 0 ≤ δ_typ)
(failure_seq : ℕ → ℝ)
(h_failure_nn : ∀ (n : ℕ), 0 ≤ failure_seq n)
(h_failure_tendsto_zero : Filter.Tendsto failure_seq Filter.atTop (nhds 0))
(h_codebook_avg_failure :
∀ {n : ℕ},
0 < n →
∑ c : ChannelCoding.Codebook ⌈Real.exp (↑n * R)⌉₊ n β,
(ChannelCoding.codebookMeasure (MeasureTheory.Measure.map (Ys 0) μ) ⌈Real.exp (↑n * R)⌉₊ n).real {c} * (MeasureTheory.Measure.pi fun (x : Fin n) => MeasureTheory.Measure.map (Xs 0) μ).real
{x : Fin n → α | (x, c (jointStronglyTypicalLossyEncoder μ Xs Ys ⋯ ε_join c x)) ∉
distortionTypicalSet μ Xs Ys d n ε_dist δ_typ} ≤ failure_seq n)
(h_slack : expectedDistortionPmf d qStar + δ_typ ≤ D + ε' / 2)
:
Used by
Achievability from a codebook-average failure bound #
InformationTheory.Shannon.rate_distortion_achievability_strong_of_codebookAvgFailure
source{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSingletonClass α]
[Fintype β]
[DecidableEq β]
[Nonempty β]
[MeasurableSingletonClass β]
(P_X_pmf : α → ℝ)
(d : DistortionFn α β)
{D : ℝ}
(qStar : α × β → ℝ)
(hqStar_mem : qStar ∈ RDConstraint P_X_pmf d D)
{R : ℝ}
(hI_lt_R : mutualInfoPmf qStar < R)
{ε' : ℝ}
(hε' : 0 < ε')
(ε_join ε_dist δ_typ : ℝ)
(hδ_typ : 0 ≤ δ_typ)
(failure_seq : ℕ → ℝ)
(h_failure_nn : ∀ (n : ℕ), 0 ≤ failure_seq n)
(h_failure_tendsto_zero : Filter.Tendsto failure_seq Filter.atTop (nhds 0))
(h_codebook_avg_failure :
∀ {n : ℕ},
0 < n →
∑ c : ChannelCoding.Codebook ⌈Real.exp (↑n * R)⌉₊ n β,
(ChannelCoding.codebookMeasure (MeasureTheory.Measure.map (ChannelCoding.iidYs 0) (rdAmbient qStar))
⌈Real.exp (↑n * R)⌉₊ n).real
{c} * (MeasureTheory.Measure.pi fun (x : Fin n) =>
MeasureTheory.Measure.map (ChannelCoding.iidXs 0) (rdAmbient qStar)).real
{x : Fin n → α | (x, c
(jointStronglyTypicalLossyEncoder (rdAmbient qStar) ChannelCoding.iidXs ChannelCoding.iidYs ⋯
ε_join c x)) ∉
distortionTypicalSet (rdAmbient qStar) ChannelCoding.iidXs ChannelCoding.iidYs d n ε_dist δ_typ} ≤ failure_seq n)
(h_slack : expectedDistortionPmf d qStar + δ_typ ≤ D + ε' / 2)
:
Rate-distortion achievability with jointStronglyTypicalLossyEncoder as the
encoder, from a codebook-averaged distortion-atypicality failure sequence
failure_seq that tends to zero.
Used by
Codebook-averaged source-failure sequence (strong-encoder variant) #
InformationTheory.Shannon.codebookAvgFailureStrong
source{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[Fintype α]
[DecidableEq α]
[Fintype β]
[DecidableEq β]
(qStar : α × β → ℝ)
(d : DistortionFn α β)
(R : ℝ)
(n : ℕ)
(ε_join ε_dist δ_typ : ℝ)
:
The codebook-averaged source-failure probability for the strong lossy
encoder, at the canonical codebook size M_n := ⌈exp(n·R)⌉.
The encoder uses the inner slack ε_join for jointStronglyTypicalSet; the
failure event tests against distortionTypicalSet with outer slack
ε_dist ≥ widening(ε_join).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Used by
InformationTheory.Shannon.codebookAvgFailureStrong_nonneg
source{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[Fintype α]
[DecidableEq α]
[Nonempty α]
[MeasurableSingletonClass α]
[Fintype β]
[DecidableEq β]
[Nonempty β]
[MeasurableSingletonClass β]
(qStar : α × β → ℝ)
(d : DistortionFn α β)
(R : ℝ)
(n : ℕ)
(ε_join ε_dist δ_typ : ℝ)
:
Used by
Entropy ↔ mutualInfoPmf bridge in the rdAmbient setting #
InformationTheory.Shannon.rdAmbient_entropy_diff_eq_mutualInfoPmf
source{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[Fintype α]
[Nonempty α]
[MeasurableSingletonClass α]
[Fintype β]
[Nonempty β]
[MeasurableSingletonClass β]
(qStar : α × β → ℝ)
(hqStar_simp : qStar ∈ stdSimplex ℝ (α × β))
:
entropy (rdAmbient qStar) (ChannelCoding.iidXs 0) + entropy (rdAmbient qStar) (ChannelCoding.iidYs 0) - entropy (rdAmbient qStar) (ChannelCoding.jointSequence ChannelCoding.iidXs ChannelCoding.iidYs 0) = mutualInfoPmf qStar
For μ := rdAmbient qStar, the entropy difference
H(X) + H(Y) − H(Z) equals mutualInfoPmf qStar.
Used by
Block-law identification for rdAmbient #
InformationTheory.Shannon.rdAmbient_block_law_iidXs
source{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[Fintype α]
[Nonempty α]
[MeasurableSingletonClass α]
[Fintype β]
[Nonempty β]
[MeasurableSingletonClass β]
(qStar : α × β → ℝ)
(hqStar_simp : qStar ∈ stdSimplex ℝ (α × β))
(n : ℕ)
:
MeasureTheory.Measure.map (jointRV ChannelCoding.iidXs n) (rdAmbient qStar) = MeasureTheory.Measure.pi fun (x : Fin n) => MeasureTheory.Measure.map (ChannelCoding.iidXs 0) (rdAmbient qStar)
The X-block joint law under rdAmbient qStar equals the product of the
single-letter X-marginal. Mirrors the private block_law_X_eq_pi_p in
ChannelCodingAchievability, specialised to rdAmbient.