InformationTheory

InformationTheory.Shannon.WynerZiv.Achievability.SourceTransport

source

Imports 2

Wyner–Ziv achievability — source transport and distortion bridge #

Two-ambient WZ-joint regularity construction #

The per-n binned code reduces the WZ error to closed error-event atoms that each consume an i.i.d. ambient plus a regularity bundle (measurability / iIndepFun / IdentDistrib / marginal positivity / marginal identities). This section supplies those bundles from the covering data (qStar / κ'), for the two ambients the error decomposition runs on:

  • the covering ambient rdAmbient qStar on ℕ → ({x // 0 < P_X x} × Fin k) (iidXs = source, iidYs = covering codeword U) drives the covering-acceptance mass bound wz_covering_sideInfo_mass_ge (instantiated with the source in the strong-typicality role and U in the conditioning role) and the covering-failure integral wz_covering_failure_prob_le;
  • the side-information ambient rdAmbient (wzSideInfoMarginal P_XY κ') on ℕ → (Fin k × {y // 0 < P_Y y}) (iidXs = covering codeword U, iidYs = side information Y) drives the per-codeword mass bound wz_covering_codeword_sideInfo_mass_le and the codebook-confusion integral wz_codebook_confusion_expectation_le.

The first block gives a generic rdAmbient-level regularity API (reusable for either ambient); the second constructs the (U, Y)-marginal pmf wzSideInfoMarginal on the positive-Y-marginal subtype together with its simplex membership and full support (the covering side already receives hqStar_mem / hqStar_pos as hypotheses). No error-probability or decoder-correctness statement is produced here — the deliverable is pure regularity, consumed downstream by the distortion-decomposition bridge.

Source-measure change of variables α' → α #

The covering LossyCode (hypothesis hcov₁) measures its block distortion under the i.i.d. covering ambient (rdAmbient qStar).map (iidXs 0) on the source-support subtype α' := {x // 0 < P_X x}, whereas the Wyner–Ziv conclusion measures the lifted code under Measure.pi P_XY on α × β. This block reconciles the source side of that change of variables: the covering ambient's X-marginal, pushed from α' back to the full alphabet α by Subtype.val, is exactly the source X-marginal P_XY.map Prod.fst. On the support the covering X-marginal singleton is ∑_u qStar(⟨a,·⟩, u) = ∑_y P_XY{(a,y)} (by hqStar_eq and hκ'sum); off the support both sides carry zero mass. This is pure source-measure transport — no decoder, error event, or distortion function enters — the source-measure companion of the null-set decoder transport wz_expectedBlockDistortion_source_agree.

The distortion-decomposition bridge #

The bridge that the derandomize + squeeze glue consumes: it decomposes the Wyner–Ziv code's actual expected block distortion into a good-event proxy plus distortionMax · Pr[error], mirroring the rate-distortion source_avg_distortion_le_simpler (AchievabilityAsymptoticFailureDecay.lean) but for the bin conditional-typicality decoder (wzBinTypicalDecoder) threaded through wzCodeOfCoveringBinning.

theorem

InformationTheory.Shannon.wz_expectedBlockDistortion_le_of_badSet

source
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [Fintype γ] [DecidableEq γ] [Nonempty γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] {M n : ℕ} (c : WynerZivCode M n α β γ) (P_XY : MeasureTheory.Measure (α × β)) [MeasureTheory.IsProbabilityMeasure P_XY] (d : DistortionFn α γ) (B : Set (Fin n → α × β)) (P : ℝ) (hP : 0 ≤ P) (hgood : ∀ p ∉ B, blockDistortion d n (fun (i : Fin n) => (p i).1) (c.decoder (c.encoder fun (i : Fin n) => (p i).1, fun (i : Fin n) => (p i).2)) ≤ P) :
c.expectedBlockDistortion P_XY d ≤ P + distortionMax d * (MeasureTheory.Measure.pi fun (x : Fin n) => P_XY).real B

Codebook-fixed distortion decomposition for a Wyner–Ziv code. The bin-decoder analogue of the rate-distortion source_avg_distortion_le_simpler: for any Wyner–Ziv code c, any "bad set" B of source blocks, and any proxy value P ≥ 0 such that outside B the empirical block distortion is at most P, the source-averaged block distortion decomposes as P + distortionMax d · Pr[B].

This is the reusable measure-theoretic core of the Wyner–Ziv distortion analysis. It is decoder-agnostic — it applies verbatim to the bin conditional-typicality decoder threaded through wzCodeOfCoveringBinning — so the bin-decoder specifics enter only when B and P are instantiated (wz_covering_binning_distortion_decomp). Sorry-free.

Used by
    theorem

    InformationTheory.Shannon.wz_covering_binning_distortion_decomp

    source
    {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [Fintype γ] [DecidableEq γ] [Nonempty γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] {α' : Type u_5} [Fintype α'] [DecidableEq α'] [Nonempty α'] [MeasurableSpace α'] [MeasurableSingletonClass α'] {Ω : Type u_6} [MeasurableSpace Ω] {k M M₁ n : ℕ} [Nonempty (Fin k)] (μ : MeasureTheory.Measure Ω) (Us : ℕ → Ω → Fin k) (Ys : ℕ → Ω → β) (ε : ℝ) (c₁ : LossyCode M₁ n α' (Fin k)) (f : Fin M₁ → Fin M) (qf : (α × β × Fin k → ℝ) × (Fin k × β → γ)) (dα' : DistortionFn α' γ) (Q : MeasureTheory.Measure (α' × β)) [MeasureTheory.IsProbabilityMeasure Q] (P : ℝ) (hP : 0 ≤ P) :
    (wzCodeOfCoveringBinning c₁ f qf.2 (wzBinTypicalDecoder μ Us Ys ε c₁ f)).expectedBlockDistortion Q dα' ≤ P + distortionMax dα' * ((MeasureTheory.Measure.pi fun (x : Fin n) => Q).real {p : Fin n → α' × β | P < blockDistortion dα' n (fun (i : Fin n) => (p i).1) fun (i : Fin n) => qf.2 (c₁.decoder (c₁.encoder fun (j : Fin n) => (p j).1) i, (p i).2)} + (MeasureTheory.Measure.pi fun (x : Fin n) => Q).real {p : Fin n → α' × β | wzBinTypicalDecoder μ Us Ys ε c₁ f (f (c₁.encoder fun (j : Fin n) => (p j).1), fun (i : Fin n) => (p i).2) ≠ c₁.decoder (c₁.encoder fun (j : Fin n) => (p j).1)})

    Wyner–Ziv covering + binning distortion-decomposition bridge. For the covering+binning Wyner–Ziv code wzCodeOfCoveringBinning c₁ f qf.2 (bin decoder) (assembled with the bin conditional-typicality decoder), the source-averaged actual block distortion decomposes as

    𝔼[dⁿ]  ≤  P  +  distortionMax dα' · ( Pr[E1] + Pr[E2] )

    where the two error events over the source blocks Fin n → α' × β are

    • E1, the covering-distortion-failure event: the reconstruction from the true covering codeword c₁.decoder (c₁.encoder x) (via the test-channel reconstruction map qf.2 and the side information y) has block distortion exceeding the proxy budget P;
    • E2, the bin-decoder confusion event: the bin conditional-typicality decoder returns a covering word different from the true covering codeword.

    Outside E1 ∪ E2 the decoder recovers the true covering codeword, so the actual reconstruction equals the ideal one and its block distortion is ≤ P; the decomposition is then the generic wz_expectedBlockDistortion_le_of_badSet plus a union bound. This is the shape the derandomize + squeeze glue consumes: it bounds Pr[E1] by the covering-distortion typicality (hfeas + wz_covering_failure_prob_le) and Pr[E2] by the codebook-restricted confusion exponent (wz_codebook_confusion_expectation_le, fed wz_covering_codeword_sideInfo_mass_le + wzIndexBinningMeasure_collision), with the two-ambient source ↔ codebook identification.

    Non-bundled: the distortion-shape reconciliation (covering proxy dα' vs actual block distortion via qf.2) is carried by the concrete event E1 whose probability the outer glue bounds — it is not hypothesized. The bound on Pr[E1] + Pr[E2] (the real analytic work) is not a hypothesis here; only the proxy nonnegativity hP is required. Sorry-free.

    Used by

      E2-only decomposition adapters #

      The four adapters wz_perN_covering_binning_code consumes to close its inner body via sorry-free glue. Each carries an honest signature (only definitional/regularity preconditions; no error-probability, decoder-correctness, or covering lower bound is a hypothesis); all four are closed sorry-free. Composition:

      lift identity    → LHS(P_XY,d) = codeSupp.EBD Q_XY dα'
E2-only decomp   → codeSupp.EBD Q_XY dα' ≤ 𝔼_{Q_XY}[ideal via qf.2] + distortionMax·Pr[E2]
ideal = covering → 𝔼_{Q_XY}[ideal via qf.2] = c₁.EBD P_X' d'   (≤ (D+δ/2)+δ/4 by hcov₁)
E2 squeeze       → distortionMax·Pr[E2] ≤ δ/4                   (∃ good binning f, radius ε)

      Here α' := {x // 0 < P_X x}, β' := {y // 0 < P_Y y}, dα' x' g := d x'.1 g, and Q_XY := pmfToMeasure (P_XY co-restricted to α' × β) (the WZ block-distortion source).

      theorem

      InformationTheory.Shannon.wz_expectedBlockDistortion_le_ideal_add_E2

      source
      {β : Type u_2} {γ : Type u_3} [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [Fintype γ] [DecidableEq γ] [Nonempty γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] {α' : Type u_5} [Fintype α'] [DecidableEq α'] [Nonempty α'] [MeasurableSpace α'] [MeasurableSingletonClass α'] {Ω : Type u_6} [MeasurableSpace Ω] {k M M₁ n : ℕ} [Nonempty (Fin k)] (μ : MeasureTheory.Measure Ω) (Us : ℕ → Ω → Fin k) (Ys : ℕ → Ω → β) (ε : ℝ) (c₁ : LossyCode M₁ n α' (Fin k)) (f : Fin M₁ → Fin M) (rec : Fin k × β → γ) (dα' : DistortionFn α' γ) (Q : MeasureTheory.Measure (α' × β)) [MeasureTheory.IsProbabilityMeasure Q] :
      (wzCodeOfCoveringBinning c₁ f rec (wzBinTypicalDecoder μ Us Ys ε c₁ f)).expectedBlockDistortion Q dα' ≤ (∫ (p : Fin n → α' × β), blockDistortion dα' n (fun (i : Fin n) => (p i).1) fun (i : Fin n) => rec (c₁.decoder (c₁.encoder fun (j : Fin n) => (p j).1) i, (p i).2) ∂MeasureTheory.Measure.pi fun (x : Fin n) => Q) + distortionMax dα' * (MeasureTheory.Measure.pi fun (x : Fin n) => Q).real {p : Fin n → α' × β | wzBinTypicalDecoder μ Us Ys ε c₁ f (f (c₁.encoder fun (j : Fin n) => (p j).1), fun (i : Fin n) => (p i).2) ≠ c₁.decoder (c₁.encoder fun (j : Fin n) => (p j).1)}

      E2-only distortion decomposition for a covering+binning code. The E2-only refinement of wz_covering_binning_distortion_decomp: for the covering+binning code wzCodeOfCoveringBinning c₁ f rec (bin decoder), the source-averaged actual block distortion is at most the ideal (true-covering-codeword) block distortion plus distortionMax · Pr[E2], where E2 is the bin-decoder confusion event. Outside E2 the decoder recovers the true covering codeword, so the actual reconstruction equals the ideal one; inside E2 the actual distortion is ≤ distortionMax ≤ ideal + distortionMax (the ideal is nonnegative). The covering-distortion-failure event E1 of wz_covering_binning_distortion_decomp is dropped: hcov₁ supplies an expected covering distortion (not typicality), so E1 is not squeezable and the ideal term is carried as an integral, not bounded by a constant P. Decoder-agnostic and non-vacuous, with no bundled hypothesis (μ/Us/Ys/ε merely parametrize the decoder). Sorry-free.

      @audit:ok

      Used by
        theorem

        InformationTheory.Shannon.wz_lift_expectedBlockDistortion_eq

        source
        {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [Fintype γ] [DecidableEq γ] [Nonempty γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] (P_XY : MeasureTheory.Measure (α × β)) [MeasureTheory.IsProbabilityMeasure P_XY] (d : DistortionFn α γ) {M n : ℕ} (x₀ : { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} }) (codeSupp : WynerZivCode M n { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } β γ) :
        (wzLiftSupportCode P_XY x₀ codeSupp).expectedBlockDistortion P_XY d = codeSupp.expectedBlockDistortion (ChannelCoding.pmfToMeasure fun (p : { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × β) => P_XY.real {(↑p.1, p.2)}) fun (x' : { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} }) (g : γ) => d (↑x') g

        Source-support lift distortion identity. The lifted Wyner–Ziv code's expected block distortion under P_XY equals the support-restricted code's expected block distortion under the co-restricted source measure Q_XY := pmfToMeasure (P_XY on α' × β) with the co-restricted distortion dα' x' g := d x'.1 g. Pure source-measure change of variables (α' → α) along φ = (Subtype.val, id) ((Q_XY)^n.map φ = P_XY^n, off-support X-atoms null both sides via wz_QXY_mem_stdSimplex); the distortion-side companion of wz_covering_source_measure_map_val_eq and the null-set transport wz_expectedBlockDistortion_source_agree. Sorry-free.

        @audit:ok

        Used by
          theorem

          InformationTheory.Shannon.wz_ideal_expectation_eq_covering

          source
          {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [Fintype γ] [DecidableEq γ] [Nonempty γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] (P_XY : MeasureTheory.Measure (α × β)) [MeasureTheory.IsProbabilityMeasure P_XY] (d : DistortionFn α γ) {k M₁ n : ℕ} (κ' : α → Fin k → ℝ) (hκ'sum : ∀ (x : α), ∑ u : Fin k, κ' x u = 1) (qStar : { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × Fin k → ℝ) (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)}) (hqStar_mem : qStar ∈ stdSimplex ℝ ({ x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × Fin k)) (d' : DistortionFn { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } (Fin k)) (qf : (α × β × Fin k → ℝ) × (Fin k × β → γ)) (hd'_eq : ∀ (x' : { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} }) (u : Fin k), d' x' u = (∑ y : β, (P_XY.real {(↑x', y)} / ∑ y' : β, P_XY.real {(↑x', y')}) * ↑(d (↑x') (qf.2 (u, y)))).toNNReal) (c₁ : LossyCode M₁ n { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } (Fin k)) :
          (∫ (p : Fin n → { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × β), blockDistortion (fun (x' : { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} }) (g : γ) => d (↑x') g) n (fun (i : Fin n) => (p i).1) fun (i : Fin n) => qf.2 (c₁.decoder (c₁.encoder fun (j : Fin n) => (p j).1) i, (p i).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)}) = c₁.expectedBlockDistortion (MeasureTheory.Measure.map (ChannelCoding.iidXs 0) (rdAmbient qStar)) d'

          Ideal distortion = covering distortion. The ideal (true covering codeword) block distortion of the binned code, integrated over the co-restricted source Q_XY, equals the covering LossyCode's expected block distortion under the i.i.d. covering ambient (rdAmbient qStar).map (iidXs 0) with the proxy distortion d'. This is the identity that lets hcov₁'s covering bound bound the ideal term.

          The body reduces both finite-alphabet integrals to sums (integral_fintype + Measure.pi_singleton), splits the product source into its α'- and β-coordinate factors (arrowProdEquivProdArrow), and for each source sequence x marginalizes the β-coordinates one at a time (wz_prod_sum_marginalize); the reconciliation hd'_eq (d' = 𝔼_{Y|X}[d ∘ qf.2], cleared by the positive X-marginal via wz_ideal_marg_mul_dprime) and the source-marginal identity wz_ideal_PX_real turn the ideal per-letter distortion into the proxy distortion. Non-circular (no hypothesis is the conclusion), non-bundled (hd'_eq/hqStar_eq/hqStar_mem/hκ'sum are the reconciliation + source-consistency preconditions, not the identity itself; the Fubini + change-of-variables identity is genuine body work). Sorry-free.

          @audit:ok

          Used by