InformationTheory.Shannon.RateDistortion.AchievabilityJointTypicalEncoder

Imports 6

Rate-distortion achievability — joint-typical lossy encoder + distortion typical set #

Two pieces of infrastructure for the lossy compression chain.

Joint-typical lossy encoder #

Symmetric counterpart to ChannelCodingAchievability.jointTypicalDecoder on the encoder side of the lossy compression chain:

jointTypicalLossyEncoder — given a codebook c : Codebook M n β and a source word x : Fin n → α, returns some (Classical.choose) message index m with (x, c m) ∈ jointlyTypicalSet μ Xs Ys n ε. Falls back to ⟨0, hM⟩ if no such m exists.
lossyCodeOfCodebook — bundles the joint-typical encoder + the codebook itself as decoder into a LossyCode M n α β.
jointTypicalLossyEncoder_spec_of_exists / _of_not_exists — dif_pos / dif_neg characterisations of the two branches.

Note: unlike the channel-coding decoder side (jointTypicalDecoder), the lossy encoder does not require uniqueness of the typical match — any one is fine because the encoder's job is only to commit to a single index. Hence we use Classical.choose of ∃ m, _ rather than Classical.choose of ∃! m, _.

Distortion typical set #

The intersection of jointlyTypicalSet with the empirical-distortion constraint blockDistortion d n x y ≤ 𝔼[d(X_0, Y_0)] + δ:

expectedJointDistortion μ X Y d — Bochner integral of d(X, Y) under μ.
distortionTypicalSet μ Xs Ys d n ε δ — set of (x, y) jointly typical and whose empirical block distortion is within δ of the joint expectation.
basic structure lemmas: subset to jointlyTypicalSet, membership iff, MeasurableSet, finiteness.

References #

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

noncomputable def

InformationTheory.Shannon.jointTypicalLossyEncoder

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Fintype β] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) {M n : ℕ} (hM : 0 < M) (ε : ℝ) (c : ChannelCoding.Codebook M n β) :

(Fin n → α) → Fin M

Joint-typical lossy encoder. Given a codebook c : Codebook M n β, returns the first (any) message index m whose codeword is jointly typical with the source word x. Falls back to ⟨0, hM⟩ if no such m exists.

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

noncomputable def

InformationTheory.Shannon.lossyCodeOfCodebook

source

LossyCode M n α β

Bundle a codebook + joint-typical lossy encoder into a LossyCode. The codebook itself serves as the decoder.

Equations

InformationTheory.Shannon.lossyCodeOfCodebook μ Xs Ys hM ε c = { encoder := InformationTheory.Shannon.jointTypicalLossyEncoder μ Xs Ys hM ε c, decoder := c }

Instances For

Used by

Distortion typical set #

noncomputable def

InformationTheory.Shannon.expectedJointDistortion

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} {β : Type u_3} (μ : MeasureTheory.Measure Ω) (X : Ω → α) (Y : Ω → β) (d : DistortionFn α β) :

ℝ

Expected per-symbol distortion 𝔼_μ[d(X, Y)] as a real Bochner integral. The bound used in distortionTypicalSet references this quantity at i = 0; under stationary i.i.d. hypotheses it is independent of i.

Equations

InformationTheory.Shannon.expectedJointDistortion μ X Y d = ∫ (ω : Ω), ↑(d (X ω) (Y ω)) ∂μ

Instances For

Used by

noncomputable def

InformationTheory.Shannon.distortionTypicalSet

source

Set ((Fin n → α) × (Fin n → β))

Distortion typical set. Pairs (x, y) ∈ (Fin n → α) × (Fin n → β) that are both (a) jointly typical in the entropy sense (jointlyTypicalSet μ Xs Ys n ε) and (b) whose empirical block distortion is within δ of the joint expectation 𝔼[d(X_0, Y_0)].

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

theorem

InformationTheory.Shannon.blockDistortion_le_of_mem_distortionTypicalSet

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 α β) (n : ℕ) (ε δ : ℝ) {p : (Fin n → α) × (Fin n → β)} (h : p ∈ distortionTypicalSet μ Xs Ys d n ε δ) :

blockDistortion d n p.1 p.2 ≤ expectedJointDistortion μ (Xs 0) (Ys 0) d + δ

On distortionTypicalSet, the empirical block distortion is bounded by the joint expectation plus δ.

Used by

Lower-bound joint-AEP independent probability #

The lower-bound counterpart to ChannelCoding.jointlyTypicalSet_indep_prob_le for the single-codeword typical-match probability (Cover–Thomas). The input hypothesis is in joint-law form μ.real {ω | (jX, jY) ∈ JTS} ≥ 1 - η, as supplied by jointlyTypicalSet_prob_tendsto_one.

theorem

InformationTheory.Shannon.jointlyTypicalSet_indep_prob_ge

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [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 : ℕ) => ChannelCoding.jointSequence Xs Ys i) μ) (hidentZ : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (ChannelCoding.jointSequence Xs Ys i) (ChannelCoding.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 (ChannelCoding.jointSequence Xs Ys 0) μ).real {p}) (n : ℕ) {ε η : ℝ} (hμJTS : 1 - η ≤ μ.real {ω : Ω | (jointRV Xs n ω, jointRV Ys n ω) ∈ ChannelCoding.jointlyTypicalSet μ Xs Ys n ε}) :

(1 - η) * Real.exp (↑n * (entropy μ (ChannelCoding.jointSequence Xs Ys 0) - entropy μ (Xs 0) - entropy μ (Ys 0) - 3 * ε)) ≤ ((MeasureTheory.Measure.map (jointRV Xs n) μ).prod (MeasureTheory.Measure.map (jointRV Ys n) μ)).real (ChannelCoding.jointlyTypicalSet μ Xs Ys n ε)

Anti-direction (lower-bound) joint-AEP indep probability. The probability under the product measure μX^n × μY^n that (X̃, Ỹ) lies in the jointly typical set is bounded below by (1 - η) · exp(-n · (I + 3ε)).

See also jointlyTypicalSet_indep_prob_le.

Used by