InformationTheory.Shannon.WynerZiv.Achievability.ChosenWord

Imports 2

Wyner–Ziv achievability — covering chosen-word typicality and the joint lossy code #

theorem

InformationTheory.Shannon.wz_coveringFamily_of_testChannel

{α : 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 α γ) (R D : ℝ) (k : ℕ) (qf : (α × β × Fin k → ℝ) × (Fin k × β → γ)) (hqf : qf ∈ WynerZivFactorizableConstraint (Fin k) (fun (p : α × β) => P_XY.real {p}) (fun (a : α) (b : γ) => ↑(d a b)) D) (hobj : wzMutualInfoXU (Fin k) qf.1 - wzMutualInfoYU (Fin k) qf.1 < R) (δ : ℝ) (hδ : 0 < δ) :

∃ (q' : α × β × Fin k → ℝ) (κ' : α → Fin k → ℝ) (qStar : { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × Fin k → ℝ) (d' : DistortionFn { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } (Fin k)), (∀ (x : α) (y : β) (u : Fin k), q' (x, y, u) = κ' x u * P_XY.real {(x, y)}) ∧ (∀ (x : α) (u : Fin k), 0 < κ' x u) ∧ (∀ (x : α), ∑ u : Fin k, κ' x u = 1) ∧ wzMutualInfoXU (Fin k) q' - wzMutualInfoYU (Fin k) q' < R ∧ (∀ (p : { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × Fin k), qStar p = κ' (↑p.1) p.2 * ∑ y : β, P_XY.real {(↑p.1, y)}) ∧ (∀ (p : { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × Fin k), 0 < qStar p) ∧ qStar ∈ stdSimplex ℝ ({ x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } × Fin k) ∧ expectedDistortionPmf d' qStar ≤ D + δ ∧ (∀ (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) ∧ qf ∈ WynerZivFactorizableConstraint (Fin k) (fun (p : α × β) => P_XY.real {p}) (fun (a : α) (b : γ) => ↑(d a b)) D ∧ ∀ (R₁ : ℝ), mutualInfoPmf qStar < R₁ → ∀ (ε' : ℝ), 0 < ε' → ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∃ (M : ℕ), ⌈Real.exp (↑n * R₁)⌉₊ ≤ M ∧ ↑M ≤ Real.exp (↑n * R₁) + 1 ∧ ∃ (c : LossyCode M n { x : α // 0 < ∑ y : β, P_XY.real {(x, y)} } (Fin k)), c.expectedBlockDistortion (MeasureTheory.Measure.map (ChannelCoding.iidXs 0) (rdAmbient qStar)) d' ≤ D + δ + ε' ∧ (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 ε) ≤ δ / (8 * (distortionMax d + 1))

Builds the covering LossyCode family from a feasible test channel. Perturbs the feasible factorizable test channel qf to a full-support kernel κ' (wz_fullKernelSupport_perturbation), restricts the covering source to the support subtype α' := {x // 0 < P_X x}, and produces the rate-distortion covering LossyCode family (wz_covering_lossyCode_exists) for the proxy distortion d' (the Y-conditional expectation of d ∘ qf.2).

The output packages, for downstream binning, the perturbed full-support factorizable joint q' (with kernel κ'), the restricted covering joint qStar, the covering proxy d', the Wyner–Ziv objective margin < R, and — for every covering rate R₁ strictly above the covering mutual information mutualInfoPmf qStar — the covering LossyCode family with block distortion within (D + δ) + ε'. The covering-distortion feasibility expectedDistortionPmf d' qStar ≤ D + δ is the reconciliation identity (wz_coveringDistortion_reconcile) applied to the perturbation's distortion bound. All conclusions are genuinely constructed; the only preconditions are feasibility (hqf), the objective margin (hobj), and the slack δ. The output existential also exports, alongside d', the reconciliation identity hd'_eq (d' = the Y-conditional expectation of d ∘ qf.2, discharged by rfl since the witness is that expression) and the test channel's factorizability hqf (the original input membership), so downstream binning can honestly relate the covering proxy d' to the real distortion d via qf.2.

The LossyCode family conclusion also exports, for the returned code c, a covering-acceptance failure mass bound at a radius ε that is a universal binder (∀ R₁ …, ∀ ε' …, ∀ ε, 0 < ε → ∃ N …). The product source–side measure of wzCoveringAcceptFailSet P_XY κ' c ε (the event that the true covering word is not jointly typical with the side information) is ≤ δ / (8 · (distortionMax d + 1)), a fixed vanishing tolerance. Because ε is a family binder, the caller chooses the same ε it feeds the bin-decoder radius, so the union bound C2 ⊆ E2 uses a matching radius. The covering-acceptance failure C2 is the true-word joint-AEP failure and decays to 0; it is the covering half of the Wyner–Ziv E2 error event, threaded to wz_exists_binning_E2_bound and discharged by construction (the distortionMax d scaling only sizes the tolerance so dMax · Pr[C2] is absorbable).

The covering-acceptance conjunct is discharged by the joint derandomize wz_covering_lossyCode_joint_exists, which produces — for the same code — a low block distortion (≤ (D+δ)+ε') and a small strong-covering-failure mass (SRC(wzCoveringSuccessStrong)ᶜ ≤ tol/2). The strong-Ecov Markov-core leaf wz_covering_chosenWord_sideInfo_typical then turns that covering-success complement bound into the acceptance-failure bound ≤ tol = δ/(8·(distortionMax d + 1)). The joint derandomize couples the distortion-typicality failure (drives block distortion via source_avg_distortion_le_simpler_generic) and the strong-joint-typicality failure at the encoder radius ε_join (drives covering-success via wz_coveringSuccessStrong_compl_measureReal_le + the measure alignment wz_covering_SRC_map_Xproj_eq and radius bridge wz_jointStrongly_mem_coveringSuccessJoint): both codebook-averaged failures are bounded by the shared vanishing upper (P_X n){Xⁿ ∉ T*_X} + exp(-Mₙ·exp(-n(I+slack))), and exists_codebook_low_avg on their sum extracts one codebook good for both. The strong covering-success lower bound rests on the gateway wz_covering_strongTypical_indep_mass_ge (the WZ instance of jointStronglyTypicalSet_indep_prob_ge). The covering-success event is wzCoveringSuccessStrong (strong-at-ε_cov ∩ weak-at-ε), which makes the Markov-core chain true-as-framed.

The good code is genuinely constructed (perturb to a full-support kernel → restricted qStar → codebook-average + exists_codebook_low_avg pigeonhole in wz_covering_lossyCode_joint_exists, then the strong-Ecov leaf), not a bundled *Hypothesis. The closure rests on strong typicality at the separated radius ε_cov = ε/(2(1+C)) (wzCoveringStrongRadius, positive), with the weak-at-ε conjunct a strong ⟹ weak plumbing consequence.

@audit:ok

Used by