Second-moment core of the mutual covering lemma #

Marton's mutual covering lemma asserts that among the M₁ * M₂ pairs formed from two independently drawn codebooks, at least one pair is jointly typical. The standard proof is a second moment argument, and its analytic core does not mention typicality at all: it only needs a measurable set S in the product alphabet and the fact that indicator variables attached to two pairs sharing no index are independent.

This file develops that core for an abstract S, in two strengths. The crude estimate uses no information about S beyond p, and its conclusion needs both M₁ p and M₂ p to be large. The sharpened estimate additionally assumes that every conditional slice of S has mass at most qbar, and its conclusion splits into a term needing only the product M₁ M₂ p to be large plus two terms carrying the ratio qbar / p.

Main definitions #

• codebookFamily X Y — the two codebooks interleaved into one family indexed by Fin M₁ ⊕ Fin M₂, so that mutual independence of all M₁ + M₂ codewords is a single iIndepFun hypothesis.
• pairIndicator X Y S p — indicator of "the codeword pair indexed by p lands in S".
• pairCount X Y S — number of codeword pairs landing in S.
• pairProb μX μY S — probability that one independently drawn pair lands in S.
• sharedFstSet S / sharedSndSet S — the triples of codewords realizing two pairs that share one index.

Main statements #

• integral_pairCount — the first moment E[A] = M₁ * M₂ * p.
• covariance_pairIndicator_eq_zero — covariance vanishes for pairs sharing no index.
• variance_pairCount_le — the resulting variance bound Var[A] ≤ M₁ M₂ (M₁ + M₂) p.
• meas_pairCount_eq_zero_le — Chebyshev's inequality applied to the above: P(A = 0) ≤ (M₁ + M₂) / (M₁ M₂ p).
• covariance_pairIndicator_shared_le — under a uniform slice bound qbar, the covariance of two pairs sharing one index is at most qbar * p.
• variance_pairCount_le' and meas_pairCount_eq_zero_le' — the sharpened variance bound Var[A] ≤ M₁ M₂ p + M₁ M₂ (M₁ + M₂) qbar p and the estimate it yields, P(A = 0) ≤ 1 / (M₁ M₂ p) + qbar / (M₁ p) + qbar / (M₂ p).

Sharpened variance bound under a uniform slice bound #

variance_pairCount_le bounds the covariance of two pairs sharing one index by the crude pairProb μX μY S. If instead every conditional slice of S has mass at most qbar, that covariance is bounded by qbar * pairProb μX μY S, and the resulting Chebyshev estimate splits into a diagonal term 1 / (M₁ M₂ p) plus shared-index terms carrying a factor qbar.

Two slice bounds are needed, one in each coordinate: the α-slices control the pairs sharing their second index and the β-slices control the pairs sharing their first index. Neither bound implies the other.

A canonical ambient realizing the hypotheses #

meas_pairCount_eq_zero_le is stated over an abstract probability space. This section exhibits the i.i.d. codebook ambient on which its hypotheses hold, so that the abstract statement is known to be non-vacuous and downstream users have a template to instantiate.