Theorem 5, the n + 2-variable Zhang-Yeung generalization

Theorem 5 of [@zhangyeung1998, §III, eqs. 27-28] extends the four-variable Zhang-Yeung inequality to a family X : ∀ i : Fin n, Ω → S i of n side variables. The asymmetric point form fixes one distinguished index i : Fin n; the averaged symmetric form follows by summing over i and dividing by n.

Main statements

• ZhangYeung.theorem5: paper eq. (27), the asymmetric Fin n-indexed form.
• ZhangYeung.theorem5_averaged: paper eq. (28), the averaged symmetric form.

Implementation notes

The proof follows the same copy-lemma chase as ZhangYeung.theorem3, but applies condIndep_copies once at the tuple codomain ∀ j : Fin n, S j. The tuple-level conditional independence is projected down to each pair (X' i, XstarCoord k), those pairwise delta bounds are summed over k, and the resulting n-ary mutual-information sum is controlled by a local chain-rule lemma mutualInfo_add_n_way_inequality.

Internally the chase runs in (Z, U) order to match delta; the public statement is rewritten to the paper's I[U : Z] order at the end via mutualInfo_comm and condMutualInfo_comm.

References

• [@zhangyeung1998, §III, Theorem 5, eqs. 27-28] -- see references/transcriptions/zhangyeung1998.md for a verbatim transcription of the theorem statement, verified 2026-04-16.

Tags

Shannon entropy, mutual information, non-Shannon information inequality, Zhang-Yeung, conditional independence

theorem ZhangYeung.theorem5 {Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} {S_U S_Z : Type u} {S : Fin n → Type u} [MeasurableSpace S_U] [MeasurableSpace S_Z] [(i : Fin n) → MeasurableSpace (S i)] [Finite S_U] [Finite S_Z] [∀ (i : Fin n), Finite (S i)] [MeasurableSingletonClass S_U] [MeasurableSingletonClass S_Z] [∀ (i : Fin n), MeasurableSingletonClass (S i)] {U : Ω → S_U} {Z : Ω → S_Z} {X : (i : Fin n) → Ω → S i} (hU : Measurable U) (hZ : Measurable Z) (hX : ∀ (i : Fin n), Measurable (X i)) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (i : Fin n) : 2 ≤ n → ↑n * I[U : Z; μ] - ∑ j : Fin n, I[U : Z|X j;μ] - ↑n * I[U : Z|X i;μ] ≤ I[X i : prod U Z; μ] + ∑ j : Fin n, H[X j; μ] - H[fun (ω : Ω) (j : Fin n) => X j ω; μ]

Theorem 5 of [@zhangyeung1998, §III, eq. 27] -- the n + 2-variable Zhang-Yeung inequality, indexed by a distinguished coordinate i : Fin n.

theorem ZhangYeung.theorem5_averaged {Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} {S_U S_Z : Type u} {S : Fin n → Type u} [MeasurableSpace S_U] [MeasurableSpace S_Z] [(i : Fin n) → MeasurableSpace (S i)] [Finite S_U] [Finite S_Z] [∀ (i : Fin n), Finite (S i)] [MeasurableSingletonClass S_U] [MeasurableSingletonClass S_Z] [∀ (i : Fin n), MeasurableSingletonClass (S i)] (hn : 2 ≤ n) {U : Ω → S_U} {Z : Ω → S_Z} {X : (i : Fin n) → Ω → S i} (hU : Measurable U) (hZ : Measurable Z) (hX : ∀ (i : Fin n), Measurable (X i)) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : ↑n * I[U : Z; μ] - 2 * ∑ j : Fin n, I[U : Z|X j;μ] ≤ 1 / ↑n * ∑ i : Fin n, I[X i : prod U Z; μ] + ∑ j : Fin n, H[X j; μ] - H[fun (ω : Ω) (j : Fin n) => X j ω; μ]

Theorem 5 of [@zhangyeung1998, §III, eq. 28] -- the averaged symmetric form of the n + 2-variable Zhang-Yeung inequality.