InformationTheory.Shannon.RateDistortion.Achievability

Imports 6

Rate-distortion achievability — structure and pmf-direct `R(D)` #

The structural layer for the achievability half of Cover–Thomas: block lossy codes and the pmf-direct rate-distortion function with its compactness / continuity / minimizer-existence apparatus.

Main definitions #

DistortionFn α β — a single-symbol distortion α → β → ℝ≥0.
blockDistortion d n x y — the block distortion (1/n) ∑ d(xᵢ, yᵢ).
LossyCode M n α β — a block lossy code (deterministic encoder + decoder).
LossyCode.expectedBlockDistortion — its expected block distortion.
expectedDistortionPmf d q — pmf-form expected distortion ∑ q(a,b) · d(a,b).
marginalFst / marginalSnd — the marginals of a joint pmf.
RDConstraint P_X d D — the feasible joint-pmf set.
mutualInfoPmf q — mutual information in entropy form H(fst) + H(snd) − H(q).
rateDistortionFunctionPmf P_X d D — the pmf-direct rate-distortion function.

Main statements #

RDConstraint_isClosed / RDConstraint_isCompact — closedness and compactness of the feasible set.
rateDistortionFunctionPmf_attained — the infimum is attained on a non-empty feasible set.

Implementation notes #

Mutual information is defined in the negMulLog entropy form H(X) + H(Y) − H(X, Y): it is a finite sum of Real.negMulLog, hence continuous on all of α × β → ℝ (Real.continuous_negMulLog). The KL / log-ratio form is avoided because its continuity breaks at zero marginals.
RDConstraint is a subset of Set (α × β → ℝ): an affine constraint on the standard simplex of α × β, closed and convex, so IsCompact.exists_isMinOn applies directly.

Distortion function #

abbrev

InformationTheory.Shannon.DistortionFn

source

@[reducible, inline]

(α : Type u_4) (β : Type u_5) :

Type (max u_4 u_5)

A single-symbol distortion function d : α → β → ℝ≥0.

Equations

InformationTheory.Shannon.DistortionFn α β = (α → β → NNReal)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.blockDistortion

source

{α : Type u_4} {β : Type u_5} (d : DistortionFn α β) (n : ℕ) (x : Fin n → α) (y : Fin n → β) :

ℝ

The block distortion dⁿ((xᵢ), (yᵢ)) := (1/n) ∑ d(xᵢ, yᵢ), valued in ℝ.

Equations

InformationTheory.Shannon.blockDistortion d n x y = 1 / ↑n * ∑ i : Fin n, ↑(d (x i) (y i))

Instances For

Used by

theorem

InformationTheory.Shannon.blockDistortion_nonneg

source

{α : Type u_4} {β : Type u_5} (d : DistortionFn α β) (n : ℕ) (x : Fin n → α) (y : Fin n → β) :

0 ≤ blockDistortion d n x y

Used by

Block lossy code #

structure

InformationTheory.Shannon.LossyCode

source

(M n : ℕ) (α : Type u_4) (β : Type u_5) [MeasurableSpace α] [MeasurableSpace β] :

Type (max u_4 u_5)

A block lossy code of length n with M codewords over source alphabet α and reconstruction alphabet β: a deterministic encoder (Fin n → α) → Fin M and decoder Fin M → (Fin n → β).

encoder : (Fin n → α) → Fin M
decoder : Fin M → Fin n → β

Instances For

Used by

noncomputable def

InformationTheory.Shannon.LossyCode.expectedBlockDistortion

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {M n : ℕ} (c : LossyCode M n α β) (P_X : MeasureTheory.Measure α) (d : DistortionFn α β) :

ℝ

Expected block distortion of a lossy code under an i.i.d. source P_X on α.

Equations

c.expectedBlockDistortion P_X d = ∫ (x : Fin n → α), InformationTheory.Shannon.blockDistortion d n x (c.decoder (c.encoder x)) ∂MeasureTheory.Measure.pi fun (x : Fin n) => P_X

Instances For

Used by

theorem

InformationTheory.Shannon.LossyCode.expectedBlockDistortion_nonneg

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {M n : ℕ} (c : LossyCode M n α β) (P_X : MeasureTheory.Measure α) (d : DistortionFn α β) :

0 ≤ c.expectedBlockDistortion P_X d

Expected block distortion is non-negative.

Used by

pmf-form expected distortion, marginals, and feasible set #

noncomputable def

InformationTheory.Shannon.expectedDistortionPmf

source

{α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (d : DistortionFn α β) (q : α × β → ℝ) :

ℝ

pmf-form expected distortion ∑ a, b, q(a,b) · d(a,b) for a joint pmf q : α × β → ℝ and NNReal-valued distortion d.

Equations

InformationTheory.Shannon.expectedDistortionPmf d q = ∑ a : α, ∑ b : β, q (a, b) * ↑(d a b)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.marginalFst

source

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

α → ℝ

First (source-side) marginal of a joint pmf q : α × β → ℝ.

Equations

InformationTheory.Shannon.marginalFst q a = ∑ b : β, q (a, b)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.marginalSnd

source

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

β → ℝ

Second (reconstruction-side) marginal of a joint pmf q : α × β → ℝ.

Equations

InformationTheory.Shannon.marginalSnd q b = ∑ a : α, q (a, b)

Instances For

Used by

theorem

InformationTheory.Shannon.continuous_expectedDistortionPmf

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Fintype β] (d : DistortionFn α β) :

Continuous fun (q : α × β → ℝ) => expectedDistortionPmf d q

Continuity of expectedDistortionPmf in q (linear in finite sum).

Used by

theorem

InformationTheory.Shannon.continuous_marginalFst

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Fintype β] :

Continuous fun (q : α × β → ℝ) => marginalFst q

Continuity of marginalFst in q.

Used by

theorem

InformationTheory.Shannon.continuous_marginalSnd

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Fintype β] :

Continuous fun (q : α × β → ℝ) => marginalSnd q

Continuity of marginalSnd in q.

Used by

def

InformationTheory.Shannon.RDConstraint

source

{α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (P_X : α → ℝ) (d : DistortionFn α β) (D : ℝ) :

Set (α × β → ℝ)

The feasible joint-pmf set {q ∈ stdSimplex | marginalFst q = P_X ∧ expectedDistortionPmf d q ≤ D}.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.RDConstraint_subset_stdSimplex

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Fintype β] (P_X : α → ℝ) (d : DistortionFn α β) (D : ℝ) :

RDConstraint P_X d D ⊆ stdSimplex ℝ (α × β)

RDConstraint ⊆ stdSimplex ℝ (α × β).

Used by

theorem

InformationTheory.Shannon.RDConstraint_isClosed

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Fintype β] (P_X : α → ℝ) (d : DistortionFn α β) (D : ℝ) :

IsClosed (RDConstraint P_X d D)

RDConstraint is closed: intersection of closed sets (stdSimplex closed, linear constraints closed).

Used by

theorem

InformationTheory.Shannon.RDConstraint_isCompact

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Fintype β] (P_X : α → ℝ) (d : DistortionFn α β) (D : ℝ) :

IsCompact (RDConstraint P_X d D)

RDConstraint is compact (closed subset of compact stdSimplex).

Used by

pmf-form mutual information (entropy form, continuous via `negMulLog`) #

noncomputable def

InformationTheory.Shannon.mutualInfoPmf

source

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

ℝ

mutualInfoPmf q := H(fst) + H(snd) − H(joint) written via negMulLog: I(X;Y) = ∑_a negMulLog(q.fst a) + ∑_b negMulLog(q.snd b) − ∑_{a,b} negMulLog(q(a,b)). This formulation is continuous on all of α × β → ℝ because Real.negMulLog is continuous everywhere (with negMulLog 0 = 0).

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.continuous_mutualInfoPmf

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Fintype β] :

Continuous fun (q : α × β → ℝ) => mutualInfoPmf q

mutualInfoPmf is continuous on α × β → ℝ.

Used by

pmf-form rate-distortion function `R(D)` #

noncomputable def

InformationTheory.Shannon.rateDistortionFunctionPmf

source

{α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (P_X : α → ℝ) (d : DistortionFn α β) (D : ℝ) :

ℝ

The pmf-direct rate-distortion function R(D) := sInf {mutualInfoPmf q | q ∈ RDConstraint P_X d D}. When the constraint set is non-empty the infimum is attained (rateDistortionFunctionPmf_attained), since RDConstraint is compact and mutualInfoPmf is continuous.

The sInf of the image is used (rather than the predicate ⨅) to avoid the ConditionallyCompleteLattice BddBelow side conditions of ⨅ q ∈ S, f q over ℝ.

Equations

InformationTheory.Shannon.rateDistortionFunctionPmf P_X d D = sInf (InformationTheory.Shannon.mutualInfoPmf '' InformationTheory.Shannon.RDConstraint P_X d D)

Instances For

Used by

Existence of a minimizer #

theorem

InformationTheory.Shannon.rateDistortionFunctionPmf_attained

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Fintype β] (P_X : α → ℝ) (d : DistortionFn α β) (D : ℝ) (h_ne : (RDConstraint P_X d D).Nonempty) :

∃ qStar ∈ RDConstraint P_X d D, IsMinOn (fun (q : α × β → ℝ) => mutualInfoPmf q) (RDConstraint P_X d D) qStar

When the constraint set RDConstraint P_X d D is non-empty, the infimum defining rateDistortionFunctionPmf is attained by some q* ∈ RDConstraint.

Used by

InformationTheory.Shannon.RateDistortion.Achievability

Rate-distortion achievability — structure and pmf-direct R(D) #

Main definitions #

Main statements #

Implementation notes #

Distortion function #

Block lossy code #

pmf-form expected distortion, marginals, and feasible set #

pmf-form mutual information (entropy form, continuous via negMulLog) #

pmf-form rate-distortion function R(D) #

Existence of a minimizer #

Rate-distortion achievability — structure and pmf-direct `R(D)` #

pmf-form mutual information (entropy form, continuous via `negMulLog`) #

pmf-form rate-distortion function `R(D)` #