Corollary 3.6: IID covering

Open

QAlgorithms.Papers.Independent.Intakethird100.P42.iidCovering

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $q(y)P(x\mid y)$ be a probability law on finite nonempty alphabets $X,Y$ , with marginal $p(x)=\sum_yq(y)P(x\mid y)$ . Independently sample a book $D:[M]\to Y^n$ from $q^{\otimes n}$ , for an arbitrary integer $M\ge1$ . Put $P^n(x^n\mid y^n)=\prod_{j=1}^nP(x_j\mid y_j)$ .

There is an absolute constant $\kappa>0$ and a constant $c>0$ depending only on this joint law such that for every $\epsilon,\delta>0$ , all sufficiently large positive $n$ admit a book-dependent selection of normalized encoders $E_D(i\mid x^n)$ satisfying

\Pr_D\!\left\{\sum_{i,x^n}\left|\frac{P^n(x^n\mid D(i))}{M}-p^{\otimes n}(x^n)E_D(i\mid x^n)\right|\ge5\epsilon\right\}\le2\alpha\exp\!\left(-\frac{\kappa M\epsilon^3\beta}{\alpha}\right),

where $\alpha=2^{n[H(X)+c\delta]}$ and $\beta=2^{n[H(X\mid Y)-c\delta]}$ . Entropies are in bits. The threshold is independent of $M$ and the error is the full joint $\ell^1$ norm on $[M]\times X^n$ .

This is the IID joint-covering statement used to construct the stochastic encoder for channel simulation.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P42

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P42

open scoped BigOperators ComplexConjugate ENNReal

open Filter

open QAlgorithms.Papers.Independent.Dependency50.P07

open QAlgorithms.Papers.Independent.Gap48.P20

open QAlgorithms.Papers.Independent.Information100.P27 (IsProbability shannon)

attribute [local instance] Classical.decEq Classical.propDecidable

/-- PDF pp.9--10, Corollary 3.6: IID covering for every positive M. Constants
precede accuracy, blocklength and book size; alpha and beta use opposite signs. -/
theorem iidCovering :
    ∃ kappa : ℝ, 0 < kappa ∧
      ∀ (X Y : Type) [Fintype X] [Fintype Y] [Nonempty X] [Nonempty Y]
        (q : Y → ℝ) (P : Y → X → ℝ),
        IsProbability q → (∀ y, IsProbability (P y)) →
        ∃ c : ℝ, 0 < c ∧ ∀ eps > (0 : ℝ), ∀ delta > (0 : ℝ), ∃ N : ℕ,
          ∀ n ≥ N, 1 ≤ n → ∀ M : ℕ, 1 ≤ M →
            let alpha := (2 : ℝ) ^ ((n : ℝ) *
              (shannon (coveringMarginal q P) + c * delta))
            let beta := (2 : ℝ) ^ ((n : ℝ) *
              ((∑ y, q y * shannon (P y)) - c * delta))
            ∃ select : (Fin M → Copies Y n) → CoverEncoder (Copies X n) M,
              bookProbability q n M (fun book => 5 * eps ≤
                coveringError (wordProb q n) (productConditional P n) M book (select book)) ≤
                  2 * alpha * Real.exp (-kappa * M * eps ^ 3 * beta / alpha) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P42

end

Source

Channel simulation with quantum side information, arXiv:quant-ph/0611008v1, PDF p. 9, Corollary 3.6: IID covering

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

There exists a real constant $\kappa>0$ such that for every pair of finite nonempty types $X,Y$ , every probability function $q$ on $Y$ , and every family of probability functions $P_y$ on $X$ , there exists $c>0$ such that for every $\varepsilon>0,\delta>0$ there is a natural number $N$ with the following property. For every $n\ge N$ with $n\ge1$ and every natural number $M\ge1$ , write $r(x)=\sum_yq(y)P_y(x)$ , $H(a)=-\sum_za(z)\log_2a(z)$ ,

\alpha=2^{n(H(r)+c\delta)},\qquad \beta=2^{n(\sum_yq(y)H(P_y)-c\delta)}.

There exists a selection assigning to each book $b:\{0,\ldots,M-1\}\to Y^n$ an encoder $e_b(x,i)\ge0$ on $X^n\times\{0,\ldots,M-1\}$ , normalized by $\sum_{i<M}e_b(x,i)=1$ for every $x\in X^n$ , such that, on defining

E(b)=\sum_{i<M}\sum_{x\in X^n} \left|\frac{\prod_{j<n}P_{(b_i)_j}(x_j)}{M} -\left(\sum_{y\in Y^n}\prod_{j<n}q(y_j)\prod_{j<n}P_{y_j}(x_j)\right)e_b(x,i)\right|,

one has

\sum_{\substack{b:\{0,\ldots,M-1\}\to Y^n\\5\varepsilon\le E(b)}} \prod_{i<M}\prod_{j<n}q((b_i)_j) \le2\alpha\exp\!\left(-\frac{\kappa M\varepsilon^3\beta}{\alpha}\right).

Here $X^n,Y^n$ are the respective length- $n$ word spaces. The constant $\kappa$ precedes all choices of types and distributions, $c$ precedes $\varepsilon,\delta$ , and the encoder selection may depend on $n,M$ ; zero probabilities are allowed, with $\log_2 0=0$ , and no upper bounds on $\varepsilon,\delta$ are assumed.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph