InformationTheory

InformationTheory.Shannon.WynerZiv.Achievability.MarkovCore

source

Imports 2

Wyner–Ziv achievability — the Markov core #

Covering chosen-word side-information acceptance (Markov lemma) #

For the covering LossyCode c, the correlated joint source mass of the acceptance-failure event wzCoveringAcceptFailSet — the event that the chosen covering word c.decoder (c.encoder x) is not jointly typical with the side information y (with (x, y) drawn from the true joint P_XY, so x and y are correlated) — is small, given only the covering-typicality success precondition (the chosen word covers the source x, a regularity precondition on the constructed code, not the acceptance conclusion).

Its analytic core is the Markov lemma: if the chosen word u = c.decoder (c.encoder x) typically covers x and the source pair (x, y) is jointly typical, then (u, y) is jointly typical — so acceptance fails only off the (exp-small) covering-failure ∪ source-atypicality set. The measure is the correlated joint source Measure.pi (pmfToMeasure (fun (x', y) ↦ P_XY{(x'.1, y)})); crucially the covering word c.decoder (c.encoder x) is a function of the source x, so the u–y correlation that makes acceptance likely is inherited from the x–y correlation and is destroyed by fixing u independently. The lemma wz_covering_sideInfo_mass_ge (a lower bound on the independent product-Y-law slice mass) and the broadcast confusion bound bc_conditional_slice_prob_le (an upper bound on a conditional-product typical slice, the confusion/wrong-codeword direction) are on the wrong measure/direction and do not supply this.

theorem

InformationTheory.Shannon.wz_covering_chosenWord_sideInfo_typical

source
{α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (P_XY : MeasureTheory.Measure (α × β)) [MeasureTheory.IsProbabilityMeasure P_XY] {k : ℕ} (κ' : α → Fin k → ℝ) (qStar : { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × Fin k → ℝ) (ε : ℝ) (hε : 0 < ε) (tol : ℝ) (htol : 0 < tol) (hκ'_pos : ∀ (x : α) (u : Fin k), 0 < κ' x u) (hκ'_sum : ∀ (x : α), ∑ u : Fin k, κ' x u = 1) (hqStar : ∀ (p : { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × Fin k), qStar p = κ' (↑p.1) p.2 * ∑ y : β, P_XY.real {(↑p.1, y)}) :
∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (M : ℕ) (c : LossyCode M n { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } (Fin k)), (MeasureTheory.Measure.pi fun (x : Fin n) => ChannelCoding.pmfToMeasure fun (p : { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × β) => P_XY.real {(↑p.1, p.2)}).real (wzCoveringSuccessStrong P_XY κ' qStar c ε)ᶜ ≤ tol / 2 → (MeasureTheory.Measure.pi fun (x : Fin n) => ChannelCoding.pmfToMeasure fun (p : { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × β) => P_XY.real {(↑p.1, p.2)}).real (wzCoveringAcceptFailSet P_XY κ' c ε) ≤ tol

Covering chosen-word side-information acceptance (the Markov lemma). For every tolerance tol > 0 there is an N such that for n ≥ N and every covering LossyCode c whose chosen words typically cover the source (the covering-success premise, an implication hypothesis), the correlated-joint-source mass of the covering-acceptance failure wzCoveringAcceptFailSet P_XY κ' c ε (the chosen word c.decoder (c.encoder x) is not jointly typical, at radius ε, with the side information) is at most tol. This is the covering half C2 of the Wyner–Ziv error E2 (C2 ⊆ E2), whose analytic core is a correlated-joint conditional-typicality concentration bound absent from Mathlib and the codebase.

The covering-success premise is a regularity precondition on the constructed code (covering-failure mass ≤ tol/2, a property of the covering LossyCode) about a different event (the x–u covering slice) than the conclusion (the u–y acceptance slice); granting it does not hand over the acceptance bound. Proved by splitting acceptance-failure ⊆ covering-failure ∪ (covering-success ∩ acceptance-failure), bounding the first part by the premise and the second by the inner wz_covering_markov_concentration, then union-bounding.

@audit:ok

Used by
    theorem

    InformationTheory.Shannon.wz_jointStrongly_mem_coveringSuccessJoint

    source
    {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (P_XY : MeasureTheory.Measure (α × β)) [MeasureTheory.IsProbabilityMeasure P_XY] {k : ℕ} [Nonempty (Fin k)] [Nonempty { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} }] (qStar : { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × Fin k → ℝ) (hmem : qStar ∈ stdSimplex ℝ ({ x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × Fin k)) {n : ℕ} (hn : 0 < n) {ε_enc ε_cov ε : ℝ} (hε_enc_nn : 0 ≤ ε_enc) (h_le_cov : ε_enc ≤ ε_cov) (hX : ↑(Fintype.card (Fin k)) * ε_enc * logSumAbs (rdAmbient qStar) ChannelCoding.iidXs < ε) (hY : ↑(Fintype.card { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} }) * ε_enc * logSumAbs (rdAmbient qStar) ChannelCoding.iidYs < ε) (hJ : ε_enc * logSumAbs (rdAmbient qStar) (ChannelCoding.jointSequence ChannelCoding.iidXs ChannelCoding.iidYs) < ε) (x : Fin n → { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} }) (u : Fin n → Fin k) (hxu : (x, u) ∈ jointStronglyTypicalSet (rdAmbient qStar) ChannelCoding.iidXs ChannelCoding.iidYs n ε_enc) :
    (x, u) ∈ jointStronglyTypicalSet (rdAmbient qStar) ChannelCoding.iidXs ChannelCoding.iidYs n ε_cov ∧ (x, u) ∈ ChannelCoding.jointlyTypicalSet (rdAmbient qStar) ChannelCoding.iidXs ChannelCoding.iidYs n ε

    Strong joint typicality at the small encoder radius ε_enc implies both conjuncts of the covering-success event: the strong conjunct at the covering radius ε_cov (via ε_enc ≤ ε_cov and radius monotonicity) and the weak conjunct at ε (via the strong-to-weak inclusion stronglyTypicalSet_subset_typicalSet, whose widening constants are the three logSumAbs bounds). No T_X restriction is needed — the bridge is a pure set inclusion.

    @audit:ok

    Used by
      theorem

      InformationTheory.Shannon.wz_covering_SRC_map_Xproj_eq

      source
      {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (P_XY : MeasureTheory.Measure (α × β)) [MeasureTheory.IsProbabilityMeasure P_XY] {k : ℕ} [Nonempty (Fin k)] [Nonempty { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} }] (κ' : α → Fin k → ℝ) (qStar : { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × Fin k → ℝ) (hqStar_mem : qStar ∈ stdSimplex ℝ ({ x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × Fin k)) (hκ'sum : ∀ (x : α), ∑ u : Fin k, κ' x u = 1) (hqStar_eq : ∀ (p : { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × Fin k), qStar p = κ' (↑p.1) p.2 * ∑ y : β, P_XY.real {(↑p.1, y)}) (n : ℕ) :
      MeasureTheory.Measure.map (fun (p : Fin n → { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × β) (j : Fin n) => (p j).1) (MeasureTheory.Measure.pi fun (x : Fin n) => ChannelCoding.pmfToMeasure fun (p : { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × β) => P_XY.real {(↑p.1, p.2)}) = MeasureTheory.Measure.pi fun (x : Fin n) => MeasureTheory.Measure.map (ChannelCoding.iidXs 0) (rdAmbient qStar)

      The covering source–side product measure SRC pushes forward under the block X-projection p ↦ (fun j ↦ (p j).1) to the covering ambient's block X-law Measure.pi (fun _ ↦ (rdAmbient qStar).map (iidXs 0)). The per-coordinate map is Prod.fst, so Measure.pi_map_pi reduces the claim to the single-coordinate marginal identity (pmfToMeasure P_XY').map Prod.fst = (rdAmbient qStar).map (iidXs 0), which holds because both marginals equal x ↦ ∑ y, P_XY(x.1, y) (using ∑ u, κ' x u = 1 for the qStar side).

      @audit:ok

      Used by