InformationTheory.Shannon.RateDistortion.AchievabilityJointStrongTypicality

Imports 5

Rate-distortion achievability — joint strong-typicality apparatus #

The joint strongly-typical apparatus for the strong-typicality variant of the rate-distortion achievability theorem. The construction reuses the single-axis strong typicality machinery of StrongTypicality.lean instantiated on the product alphabet α × β, with the joint sequence jointSequence Xs Ys i ω = (Xs i ω, Ys i ω).

Main definitions #

jointStronglyTypicalSet — the joint strongly-typical set over α × β.
jointStronglyTypicalLossyEncoder — a strong-JTS lossy encoder.
conditionalStronglyTypicalSlice — the Y-fiber of the joint strongly-typical set at a fixed X-block.

Main statements #

typeCount_joint_sum_snd / typeCount_joint_sum_fst — marginalisation of the joint type-count recovers the X- / Y-type-count.
jointStronglyTypicalSet_implies_X_stronglyTypical / jointStronglyTypicalSet_implies_Y_stronglyTypical — joint strong typicality implies axis strong typicality with widened slack.
jointStronglyTypicalSet_indep_prob_ge — strong-typical independent probability lower bound.

Implementation notes #

The joint-sequence i.i.d. infrastructure (iidAmbientJoint_iIndepFun_joint, iidAmbientJoint_identDistrib_joint) lives in IIDProductInput/Joint.lean; pairwise / ident-distrib of the joint sequence are taken at the statement level to keep the development abstract.

Joint strongly typical set #

noncomputable def

InformationTheory.Shannon.jointStronglyTypicalSet

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [DecidableEq α] [DecidableEq β] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) (n : ℕ) (ε : ℝ) :

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

Joint strongly typical set over the product alphabet α × β. A pair (x, y) : (Fin n → α) × (Fin n → β) is in the set iff the "reshape" fun i => (x i, y i) : Fin n → α × β lies in the single-axis strongly typical set for the joint sequence jointSequence Xs Ys.

Concretely (unfolding stronglyTypicalSet):

(x, y) ∈ jointStronglyTypicalSet μ Xs Ys n ε ↔ ∀ (a, b), |(typeCount (fun i => (x i, y i)) (a, b) : ℝ)/n - (μ.map (jointSequence Xs Ys 0)).real {(a, b)}| ≤ ε.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.mem_jointStronglyTypicalSet_iff

source

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) (n : ℕ) (ε : ℝ) (x : Fin n → α) (y : Fin n → β) :

(x, y) ∈ jointStronglyTypicalSet μ Xs Ys n ε ↔ (fun (i : Fin n) => (x i, y i)) ∈ stronglyTypicalSet μ (ChannelCoding.jointSequence Xs Ys) n ε

Used by

theorem

InformationTheory.Shannon.jointStronglyTypicalSet_finite

source

(jointStronglyTypicalSet μ Xs Ys n ε).Finite

The joint strongly typical set is finite.

Used by

Strong-typical independent probability lower bound #

Marginalisation of `typeCount` over a coordinate #

theorem

InformationTheory.Shannon.typeCount_joint_sum_snd

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] {n : ℕ} (x : Fin n → α) (y : Fin n → β) (a : α) :

∑ b : β, typeCount (fun (i : Fin n) => (x i, y i)) (a, b) = typeCount x a

Marginalising the joint type-count over β recovers the X type-count: ∑_b typeCount (fun i => (x i, y i)) (a, b) = typeCount x a.

Used by

theorem

InformationTheory.Shannon.typeCount_joint_sum_fst

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [DecidableEq β] [Nonempty β] {n : ℕ} (x : Fin n → α) (y : Fin n → β) (b : β) :

∑ a : α, typeCount (fun (i : Fin n) => (x i, y i)) (a, b) = typeCount y b

Marginalising the joint type-count over α recovers the Y type-count.

Used by

Strong joint ⟹ strong X- and Y-typicality (with widened slack) #

theorem

InformationTheory.Shannon.jointStronglyTypicalSet_implies_X_stronglyTypical

source

x ∈ stronglyTypicalSet μ Xs n (↑(Fintype.card β) * ε)

Strong joint typicality ⟹ Strong X-typicality (slack widened by |β|). Given (fun i => (x i, y i)) ∈ stronglyTypicalSet μ (jointSequence Xs Ys) n ε and (μ.map (jointSequence Xs Ys 0)).map Prod.fst = μ.map (Xs 0), we have x ∈ stronglyTypicalSet μ Xs n (Fintype.card β · ε).

Used by

theorem

InformationTheory.Shannon.jointStronglyTypicalSet_implies_Y_stronglyTypical

source

y ∈ stronglyTypicalSet μ Ys n (↑(Fintype.card α) * ε)

Strong joint typicality ⟹ Strong Y-typicality (slack widened by |α|).

Used by

Strong joint typicality probability lower bound #

theorem

InformationTheory.Shannon.jointStronglyTypicalSet_indep_prob_ge

source

∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → (1 - η) * Real.exp (↑n * (entropy μ (ChannelCoding.jointSequence Xs Ys 0) - entropy μ (Xs 0) - entropy μ (Ys 0) - (↑(Fintype.card β) * ε * logSumAbs μ Xs + ↑(Fintype.card α) * ε * logSumAbs μ Ys + ε * logSumAbs μ (ChannelCoding.jointSequence Xs Ys) + 3 * δ))) ≤ ((MeasureTheory.Measure.map (jointRV Xs n) μ).prod (MeasureTheory.Measure.map (jointRV Ys n) μ)).real (jointStronglyTypicalSet μ Xs Ys n ε)

Strong-typical independent probability lower bound (mirror of jointlyTypicalSet_indep_prob_ge for the strong-typicality version).

For an i.i.d. joint sequence with marginals matching μ.map (Xs 0) and μ.map (Ys 0), and any η > 0, eventually for all n large enough,

(1 - η) · exp(n · ((H(Z) - H(X) - H(Y)) - ((Fintype.card β · L_X + Fintype.card α · L_Y + L_Z) · ε + 3 δ))) ≤ (μ_X^n × μ_Y^n).real (jointStronglyTypicalSet ε),

where L_X := logSumAbs μ Xs, L_Y := logSumAbs μ Ys, L_Z := logSumAbs μ (jointSequence Xs Ys), and δ > 0 is an arbitrary auxiliary slack.

Compared to the weak version's 3ε slack, the strong version has slack (Fintype.card β · L_X + Fintype.card α · L_Y + L_Z) · ε + 3 δ because converting from the strong joint typicality (slack ε) to weak X/Y/joint typicality (slack < ε') through stronglyTypicalSet_subset_typicalSet amplifies ε by the Lipschitz constant.

Used by

Strong-JTS lossy encoder #

noncomputable def

InformationTheory.Shannon.jointStronglyTypicalLossyEncoder

source

(Fin n → α) → Fin M

Strong-JTS lossy encoder. Parallel to jointTypicalLossyEncoder but targets jointStronglyTypicalSet. Given a codebook c, returns some index m with (x, c m) ∈ jointStronglyTypicalSet; falls back to ⟨0, hM⟩ otherwise.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.jointStronglyTypicalLossyEncoder_spec_of_exists

source

(x, c (jointStronglyTypicalLossyEncoder μ Xs Ys hM ε c x)) ∈ jointStronglyTypicalSet μ Xs Ys n ε

If a strong-JTS match exists for x, the strong encoder returns one.

Used by

Conditional strong-typical slice #

The Y-fiber mass of the joint strongly-typical set under the product measure μ_Y^n is lower-bounded for x X-axis strongly typical: this is the strong-typicality dual of SlepianWolfConditionalTypicalSlice.conditionalTypicalSlice_card_le (an upper bound on the X-fiber of jointlyTypicalSet). The cardinality is lower-bounded via stronglyTypicalSet_card_ge_eventually on Z and the individual fiber masses upper-bounded via typicalSet_prob_le on Y, yielding the per-source-typical match-probability lower bound exp(-n(I(X;Y) + δ(ε))) of Cover–Thomas.

noncomputable def

InformationTheory.Shannon.conditionalStronglyTypicalSlice

source

Set (Fin n → β)

Conditional strong-typical slice. For a fixed X-block x : Fin n → α, the Y-fiber of the joint strongly-typical set at x.

Equations

InformationTheory.Shannon.conditionalStronglyTypicalSlice μ Xs Ys n ε x = {y : Fin n → β | (x, y) ∈ InformationTheory.Shannon.jointStronglyTypicalSet μ Xs Ys n ε}

Instances For

Used by

theorem

InformationTheory.Shannon.mem_conditionalStronglyTypicalSlice_iff

source

y ∈ conditionalStronglyTypicalSlice μ Xs Ys n ε x ↔ (x, y) ∈ jointStronglyTypicalSet μ Xs Ys n ε

Used by

The rate-distortion achievability theorem is assembled in AchievabilityStrongTypicality.lean via the strong-encoder track (codebookAvgFailureStrong_tendsto_zero + rate_distortion_achievability_strong), which uses the conditional method-of-types directly; the public theorem rate_distortion_achievability lives in that file.

InformationTheory.Shannon.RateDistortion.AchievabilityJointStrongTypicality

Rate-distortion achievability — joint strong-typicality apparatus #

Main definitions #

Main statements #

Implementation notes #

Joint strongly typical set #

Strong-typical independent probability lower bound #

Marginalisation of typeCount over a coordinate #

Strong joint ⟹ strong X- and Y-typicality (with widened slack) #

Strong joint typicality probability lower bound #

Strong-JTS lossy encoder #

Conditional strong-typical slice #

Marginalisation of `typeCount` over a coordinate #