InformationTheory.Shannon.RateDistortion.AchievabilityStrongTypicality

Imports 8

Rate-distortion achievability — assembly (strong-typicality variant) #

The rate-distortion achievability theorem, assembled from the strong-encoder random-coding chain via conditionalStronglyTypicalSlice_mass_ge (ConditionalMethodOfTypes.lean), the Cover–Thomas strong-typicality conditional slice mass lower bound.

Architectural note #

The ambient-measure and witness-form wrappers (in AchievabilityAmbientMeasure.lean) hard-code the weak joint-typical lossy encoder jointTypicalLossyEncoder. The strong-typicality random-coding analysis requires the strong encoder jointStronglyTypicalLossyEncoder (from AchievabilityJointStrongTypicality.lean).

To avoid invasive refactoring of those weak-encoder-bound proofs, this file duplicates the witness-form / ambient-measure layers with the strong encoder swapped in. The duplication is mechanical: the proofs are encoder-agnostic — only blockDistortion_le_distortionMax and blockDistortion_le_of_mem_distortionTypicalSet are used.

Outline #

per_source_typical_match_prob_strong_ge — direct corollary of conditionalStronglyTypicalSlice_mass_ge, repackaged in the (Measure.pi (μ.map (Ys 0))).real form expected by the random-coding chain.
encoder_strong_failure_prob_le — codebook-averaged probability that no strong-JT match exists, integrated over x ∈ stronglyTypicalSet, bounded by exp(-M · exp(-n(I+δ))).
source_avg_distortion_le_simpler_generic — source-averaged distortion bound with arbitrary encoder parameter (verbatim mirror of source_avg_distortion_le_simpler).
lossyCodeOfCodebook_strong — strong analogue of lossyCodeOfCodebook.
rate_distortion_achievability_witness_form_strong — verbatim mirror of the weak witness form.
codebookAvgFailureStrong — codebookAvgFailure with the strong encoder.
codebookAvgFailureStrong_tendsto_zero — main probabilistic content, assembled from (1)+(2)+(3) + stronglyTypicalSet_prob_tendsto_one.
rate_distortion_achievability_strong_of_codebookAvgFailure — achievability from a codebook-average failure bound.
rate_distortion_achievability — final no-hypothesis theorem.

Positivity caveat #

conditionalStronglyTypicalSlice_mass_ge requires the joint pmf qStar to have strictly positive mass on every (a, b) ∈ α × β, so the present theorem carries (hqStar_pos : ∀ p, 0 < qStar p) as an additional hypothesis. An unconditional form would require a perturbation argument (passing qStar through qStar_ε := (1-ε)·qStar + ε·uniform and taking ε → 0).

Final theorem: `rate_distortion_achievability` #

theorem

InformationTheory.Shannon.rate_distortion_achievability_strong

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) (hqStar_pos : ∀ (p : α × β), 0 < qStar p) {R : ℝ} (hI_lt_R : mutualInfoPmf qStar < R) {ε' : ℝ} (hε' : 0 < ε') (ε_X ε_join ε_dist δ_kl δ_typ : ℝ) (hε_X_pos : 0 < ε_X) (hε_join_pos : 0 < ε_join) (hε_dist_pos : 0 < ε_dist) (hδ_kl_pos : 0 < δ_kl) (hδ_typ_nn : 0 ≤ δ_typ) (hε_X_lt_ε_join : ε_X < ε_join) (h_rate_gap : mutualInfoPmf qStar + (↑(Fintype.card α) * ε_X * logSumAbs (rdAmbient qStar) ChannelCoding.iidYs + ε_X * logSumAbs (rdAmbient qStar) ChannelCoding.iidXs + ε_X * logSumAbs (rdAmbient qStar) (ChannelCoding.jointSequence ChannelCoding.iidXs ChannelCoding.iidYs) + δ_kl) < R) (h_slack : expectedDistortionPmf d qStar + δ_typ ≤ D + ε' / 2) (h_dist_slack : ε_join * ∑ p : α × β, ↑(d p.1 p.2) ≤ δ_typ) (h_jts_subset_dts : ∀ {n : ℕ}, 0 < n → ∀ (x : Fin n → α) (y : Fin n → β), (x, y) ∈ jointStronglyTypicalSet (rdAmbient qStar) ChannelCoding.iidXs ChannelCoding.iidYs n ε_join → (x, y) ∈ distortionTypicalSet (rdAmbient qStar) ChannelCoding.iidXs ChannelCoding.iidYs d n ε_dist δ_typ) (qZ_min : ℝ) (hqZ_min_pos : 0 < qZ_min) (hqZ_min_le : ∀ (p : α × β), qZ_min ≤ (ChannelCoding.pmfToMeasure qStar).real {p}) (hδ_kl_dominates : 8 * ↑(Fintype.card α) * ↑(Fintype.card β) * ε_X ^ 2 ≤ δ_kl * qZ_min) :

∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∃ (M : ℕ) (_ : ⌈Real.exp (↑n * R)⌉₊ ≤ M) (_ : ↑M ≤ Real.exp (↑n * R) + 1) (c : LossyCode M n α β), c.expectedBlockDistortion (MeasureTheory.Measure.map (ChannelCoding.iidXs 0) (rdAmbient qStar)) d ≤ D + ε'

Rate-distortion theorem (achievability, strong-typicality form).

Given a feasible joint pmf qStar ∈ RDConstraint P_X_pmf d D with strictly positive mass on every (a, b), and a rate R > mutualInfoPmf qStar, for any tolerance ε' > 0, there exists N such that for all n ≥ N, there exists a lossy code of size ⌈exp(nR)⌉ whose expected block distortion is ≤ D + ε'.

The slack parameters ε_X, ε_join, ε_dist, δ_kl, δ_typ are exposed as explicit hypotheses to keep the slack-budgeting calculations external; a caller can choose them in any consistent way.

Restriction: hqStar_pos : ∀ p, 0 < qStar p is required by conditionalStronglyTypicalSlice_mass_ge. The unconditional formulation requires a perturbation argument (passing through qStar_τ := (1-τ)·qStar + τ·uniform, exploiting continuity of mutualInfoPmf and expectedDistortionPmf).

Used by

theorem

InformationTheory.Shannon.rate_distortion_achievability