InformationTheory.Shannon.RateDistortion.AchievabilityUnconditional

Imports 5

Rate-distortion achievability — strong-typical ⊆ distortion-typical inclusion #

This file proves the inclusion that the unconditional rate-distortion achievability chain rests on: a joint strongly-typical pair is distortion-typical,

jointStronglyTypicalSet μ Xs Ys n ε_join ⊆ distortionTypicalSet μ Xs Ys d n ε_dist δ_typ.

Since distortionTypicalSet = jointlyTypicalSet ∩ {blockDistortion ≤ 𝔼[d] + δ} (AchievabilityJointTypicalEncoder.lean), the inclusion factors into two parts:

(i) jointStronglyTypicalSet ⊆ jointlyTypicalSet — strong (per-symbol type deviation) typicality implies weak (entropy) typicality, via the existing strong-to-weak bridge stronglyTypicalSet_subset_typicalSet on each of the X-, Y-, and joint axes;
(ii) on a strongly-typical pair, the empirical block distortion stays within ε_join · ∑ d of the expected joint distortion, because |typeCount/n − q| ≤ ε_join at every letter.

The ε_join ↔ ε_dist bounds (i) and the distortion slack δ_typ ≥ ε_join · ∑ d (ii) are exposed as explicit hypotheses: they are the slack quantities the caller selects in the surrounding achievability wrapper, not the analytic core.

References #

T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.

Part (ii): empirical block distortion stays in the distortion band #

theorem

InformationTheory.Shannon.blockDistortion_le_of_mem_jointStronglyTypicalSet

source

blockDistortion d n x y ≤ expectedJointDistortion μ (Xs 0) (Ys 0) d + ε_join * ∑ p : α × β, ↑(d p.1 p.2)

Used by

Part (i): joint strong typicality implies joint (weak) typicality #

theorem

InformationTheory.Shannon.jointStronglyTypicalSet_subset_jointlyTypicalSet

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)) (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) μ) {n : ℕ} (hn : 0 < n) {ε_join ε_dist : ℝ} (hε_join : 0 ≤ ε_join) (h_bound_X : ↑(Fintype.card β) * ε_join * logSumAbs μ Xs < ε_dist) (h_bound_Y : ↑(Fintype.card α) * ε_join * logSumAbs μ Ys < ε_dist) (h_bound_Z : ε_join * logSumAbs μ (ChannelCoding.jointSequence Xs Ys) < ε_dist) :

jointStronglyTypicalSet μ Xs Ys n ε_join ⊆ ChannelCoding.jointlyTypicalSet μ Xs Ys n ε_dist

Used by

Joint strong typicality implies distortion typicality #

theorem

InformationTheory.Shannon.jts_subset_dts_of_dist_slack

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)) (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) μ) (d : DistortionFn α β) {n : ℕ} (hn : 0 < n) {ε_join ε_dist δ_typ : ℝ} (hε_join : 0 ≤ ε_join) (h_bound_X : ↑(Fintype.card β) * ε_join * logSumAbs μ Xs < ε_dist) (h_bound_Y : ↑(Fintype.card α) * ε_join * logSumAbs μ Ys < ε_dist) (h_bound_Z : ε_join * logSumAbs μ (ChannelCoding.jointSequence Xs Ys) < ε_dist) (h_dist_slack : ε_join * ∑ p : α × β, ↑(d p.1 p.2) ≤ δ_typ) :

jointStronglyTypicalSet μ Xs Ys n ε_join ⊆ distortionTypicalSet μ Xs Ys d n ε_dist δ_typ

A joint strongly typical pair is distortion typical:

jointStronglyTypicalSet μ Xs Ys n ε_join ⊆ distortionTypicalSet μ Xs Ys d n ε_dist δ_typ.

The ε_join ↔ ε_dist bounds (h_bound_X/Y/Z) and the distortion slack δ_typ ≥ ε_join · ∑ d (h_dist_slack) are the caller-supplied slack conditions of the surrounding achievability wrapper; the analytic content — strong-to-weak typicality and the empirical-distortion deviation bound — is proved here.

Used by

Marginal-preserving full-support perturbation #

The strong-typicality achievability theorem requires a strictly-positive optimal joint pmf. Starting from a minimizer qStar ∈ RDConstraint P_X d D (which may sit on the boundary of the simplex), we perturb it toward the product P_X ⊗ uniform_β,

q'(a, b) := (1 - λ) · qStar(a, b) + λ · P_X(a) / |β|.

For a full-support source P_X and 0 < λ ≤ 1 this is strictly positive everywhere, keeps the source marginal equal to P_X, and — by continuity in λ at λ = 0 — keeps mutual information below R and expected distortion within ε/4 of the constraint value.

noncomputable def

InformationTheory.Shannon.rdPerturb

source

{α : Type u_2} {β : Type u_3} [Fintype β] (qStar : α × β → ℝ) (P_X : α → ℝ) (lam : ℝ) :

α × β → ℝ

Marginal-preserving perturbation of a joint pmf qStar toward the product P_X ⊗ uniform_β: q'(a,b) := (1-λ)·qStar(a,b) + λ·P_X(a)/|β|. For 0 < λ ≤ 1 and a full-support source P_X, this is strictly positive at every point while keeping the source marginal equal to P_X.

Equations

InformationTheory.Shannon.rdPerturb qStar P_X lam p = (1 - lam) * qStar p + lam * (P_X p.1 / ↑(Fintype.card β))

Instances For

Used by

theorem

InformationTheory.Shannon.rdPerturb_mem_stdSimplex

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] {qStar : α × β → ℝ} {P_X : α → ℝ} {lam : ℝ} (hlam0 : 0 ≤ lam) (hlam1 : lam ≤ 1) (hqStar : qStar ∈ stdSimplex ℝ (α × β)) (hP_X : P_X ∈ stdSimplex ℝ α) :

rdPerturb qStar P_X lam ∈ stdSimplex ℝ (α × β)

Used by

theorem

InformationTheory.Shannon.rdPerturb_pos

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] {qStar : α × β → ℝ} {P_X : α → ℝ} {lam : ℝ} (hlam0 : 0 < lam) (hlam1 : lam ≤ 1) (hqStar : qStar ∈ stdSimplex ℝ (α × β)) (hP_supp : ∀ (a : α), 0 < P_X a) (p : α × β) :

0 < rdPerturb qStar P_X lam p

Used by

theorem

InformationTheory.Shannon.rdPerturb_marginalFst

source

marginalFst (rdPerturb qStar P_X lam) = P_X

Used by

theorem

InformationTheory.Shannon.rdPerturb_mutualInfo_lt

source

∃ (lam₀ : ℝ), 0 < lam₀ ∧ lam₀ ≤ 1 ∧ ∀ (lam : ℝ), 0 < lam → lam ≤ lam₀ → mutualInfoPmf (rdPerturb qStar P_X lam) < R

Used by

theorem

InformationTheory.Shannon.rdPerturb_expectedDist_le

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] {qStar : α × β → ℝ} {P_X : α → ℝ} {d : DistortionFn α β} {D ε : ℝ} (hE : expectedDistortionPmf d qStar ≤ D) (hε : 0 < ε) :

∃ (lam₁ : ℝ), 0 < lam₁ ∧ lam₁ ≤ 1 ∧ ∀ (lam : ℝ), 0 < lam → lam ≤ lam₁ → expectedDistortionPmf d (rdPerturb qStar P_X lam) ≤ D + ε / 4

Used by

Existence of consistent slack parameters #

Given a strictly-positive joint pmf q' with mutualInfoPmf q' < R and expected distortion within ε/4 of the constraint, we select the five slack parameters ε_X, ε_join, ε_dist, δ_kl, δ_typ (plus the KL floor qZ_min) that simultaneously satisfy every hypothesis of rate_distortion_achievability_strong (with the relaxation D ↦ D + ε/4, ε' ↦ ε/2) and the side conditions of jts_subset_dts_of_dist_slack. All quantities are finite constants determined by q'; the selection is pure real arithmetic, not an analytic wall.

theorem

InformationTheory.Shannon.rdSlack_exists

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] {d : DistortionFn α β} {D R ε : ℝ} {q' : α × β → ℝ} (hq'_simp : q' ∈ stdSimplex ℝ (α × β)) (hq'_pos : ∀ (p : α × β), 0 < q' p) (hI' : mutualInfoPmf q' < R) (hE' : expectedDistortionPmf d q' ≤ D + ε / 4) (hε : 0 < ε) :

∃ (ε_X : ℝ) (ε_join : ℝ) (ε_dist : ℝ) (δ_kl : ℝ) (δ_typ : ℝ) (qZ_min : ℝ), 0 < ε_X ∧ 0 < ε_join ∧ 0 < ε_dist ∧ 0 < δ_kl ∧ 0 ≤ δ_typ ∧ ε_X < ε_join ∧ mutualInfoPmf q' + (↑(Fintype.card α) * ε_X * logSumAbs (rdAmbient q') ChannelCoding.iidYs + ε_X * logSumAbs (rdAmbient q') ChannelCoding.iidXs + ε_X * logSumAbs (rdAmbient q') (ChannelCoding.jointSequence ChannelCoding.iidXs ChannelCoding.iidYs) + δ_kl) < R ∧ expectedDistortionPmf d q' + δ_typ ≤ D + ε / 4 + ε / 2 / 2 ∧ ε_join * ∑ p : α × β, ↑(d p.1 p.2) ≤ δ_typ ∧ ↑(Fintype.card β) * ε_join * logSumAbs (rdAmbient q') ChannelCoding.iidXs < ε_dist ∧ ↑(Fintype.card α) * ε_join * logSumAbs (rdAmbient q') ChannelCoding.iidYs < ε_dist ∧ ε_join * logSumAbs (rdAmbient q') (ChannelCoding.jointSequence ChannelCoding.iidXs ChannelCoding.iidYs) < ε_dist ∧ 0 < qZ_min ∧ (∀ (p : α × β), qZ_min ≤ (ChannelCoding.pmfToMeasure q').real {p}) ∧ 8 * ↑(Fintype.card α) * ↑(Fintype.card β) * ε_X ^ 2 ≤ δ_kl * qZ_min

Slack parameters ε_X, ε_join, ε_dist, δ_kl, δ_typ, qZ_min satisfying the rate gap, the distortion budget, the strong-to-weak ε-bounds and the KL-floor domination all exist simultaneously, for a strictly positive joint pmf q' whose mutual information is below R.

Used by

Source-law bridge #

theorem

InformationTheory.Shannon.rdAmbient_iidXs_eq_pmfToMeasure_source

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] {q : α × β → ℝ} (hq : q ∈ stdSimplex ℝ (α × β)) {P_X : α → ℝ} (hP : P_X ∈ stdSimplex ℝ α) (hmarg : marginalFst q = P_X) :

MeasureTheory.Measure.map (ChannelCoding.iidXs 0) (rdAmbient q) = ChannelCoding.pmfToMeasure P_X

The source-side marginal of the i.i.d. ambient built from q equals the pmfToMeasure of the source pmf P_X, provided marginalFst q = P_X. This lets the achievability conclusion be stated over pmfToMeasure P_X rather than the internal perturbed ambient.

Used by

Wrapper: unconditional operational achievability #

theorem

InformationTheory.Shannon.rate_distortion_achievability_operational

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] (P_X : α → ℝ) (hP_pmf : P_X ∈ stdSimplex ℝ α) (hP_supp : ∀ (a : α), 0 < P_X a) (d : DistortionFn α β) {D : ℝ} (h_ne : (RDConstraint P_X d D).Nonempty) {R : ℝ} (hR : rateDistortionFunctionPmf P_X d D < R) {ε : ℝ} (hε : 0 < ε) :

∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∃ (M : ℕ) (_ : ⌈Real.exp (↑n * R)⌉₊ ≤ M) (_ : ↑M ≤ Real.exp (↑n * R) + 1) (c : LossyCode M n α β), c.expectedBlockDistortion (ChannelCoding.pmfToMeasure P_X) d ≤ D + ε

Rate-distortion theorem (achievability, unconditional operational form).

For a full-support source P_X with a feasible constraint set and any rate R > R(D), for every ε > 0 there is a block length N such that every n ≥ N admits a rate-R lossy code whose expected block distortion is at most D + ε.

Unlike rate_distortion_achievability_strong, this form carries no slack, no strict-positivity of an optimal pmf, and no strong-to-weak inclusion hypothesis: they are all discharged internally via a marginal-preserving full-support perturbation (rdPerturb), the strong-to-distortion inclusion (jts_subset_dts_of_dist_slack), and the slack selection (rdSlack_exists).

hP_supp : ∀ a, 0 < P_X a is a regularity precondition, not load-bearing: it is required only so the marginal-preserving perturbation toward P_X ⊗ uniform_β lands strictly positive; the operational content is proved internally.

@audit:ok

Used by