Lemma 3.5: covering lemma

Open

QAlgorithms.Papers.Independent.Intakethird100.P42.coveringLemma

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

prove2quantum

Let $X,Y$ be finite nonempty alphabets, $q$ a probability distribution on $Y$ , and $P(\cdot\mid y)$ a probability distribution on $X$ for every $y$ . Put $p(x)=\sum_yq(y)P(x\mid y)$ . Suppose $\epsilon,K,k>0$ , $0<\eta<1$ , $T\subseteq X$ , and $T_y\subseteq X$ satisfy

\sum_yq(y)P(T_y\mid y)\ge1-\epsilon,\quad p(T)\ge1-\epsilon,\quad |T|\le K,\quad P(x\mid y)\le k^{-1}\quad(x\in T_y).

Let $M=\lceil K/(\eta k)\rceil$ and independently sample $D(1),\ldots,D(M)$ from $q$ . There is an absolute constant $\kappa>0$ and a selection, for every whole book $D$ , of a normalized conditional distribution $E_D(i\mid x)$ on $[M]$ such that

\Pr_D\!\left\{\sum_{i=1}^M\sum_x\left|\frac{P(x\mid D(i))}{M}-p(x)E_D(i\mid x)\right|\ge5\epsilon\right\}\le2K\exp(-\kappa\epsilon^3/\eta).

The constant is uniform over the data. Every encoder row is normalized, including when $p(x)=0$ ; selection may depend on the sampled book.

This compares the entire joint distribution on $[M]\times X$ in the dilution and concentration directions. The printed proof's subnormalized completion step is flagged for moderation; it is not added as a hypothesis.

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.7--9, Lemma 3.5: covering, including the ceiling, normalized encoder
and full joint l1 norm. The encoder can depend on the entire sampled book;
its selection is outside the event, not an assumption that a good encoder exists. -/
theorem coveringLemma :
    ∃ 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)) →
        ∀ (T : Finset X) (Ty : Y → Finset X) (eps K k eta : ℝ),
          0 < eps → 0 < K → 0 < k → 0 < eta → eta < 1 →
          (1 - eps ≤ ∑ y, q y * ∑ x ∈ Ty y, P y x) →
          (1 - eps ≤ ∑ y, q y * ∑ x ∈ T, P y x) →
          (T.card : ℝ) ≤ K → (∀ y x, x ∈ Ty y → P y x ≤ k⁻¹) →
          let M := ⌈K / (eta * k)⌉₊
          ∃ select : (Fin M → Y) → CoverEncoder X M,
            (∑ book : Fin M → Y,
              if 5 * eps ≤ coveringError q P M book (select book) then ∏ i, q (book i)
              else 0) ≤ 2 * K * Real.exp (-kappa * eps ^ 3 / eta) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P42

end

Source

Channel simulation with quantum side information, arXiv:quant-ph/0611008v1, PDF p. 7, Lemma 3.5: covering lemma

Read-back

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

There exists a real constant $\kappa>0$ such that the following holds 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$ . For every finite subset $T\subseteq X$ , family of finite subsets $T_y\subseteq X$ , and real numbers $\varepsilon,K,k,\eta$ satisfying $\varepsilon>0$ , $K>0$ , $k>0$ , $0<\eta<1$ ,

1-\varepsilon\le\sum_yq(y)\sum_{x\in T_y}P_y(x),\qquad 1-\varepsilon\le\sum_yq(y)\sum_{x\in T}P_y(x),\qquad |T|\le K,

and $P_y(x)\le k^{-1}$ whenever $x\in T_y$ , let $M=\lceil K/(\eta k)\rceil$ , a positive natural number. There exists a selection assigning to every book $b:\{0,\ldots,M-1\}\to Y$ an encoder $e_b(x,i)\ge0$ , with $\sum_{i<M}e_b(x,i)=1$ for every $x$ , such that

\sum_{\substack{b:\{0,\ldots,M-1\}\to Y\\ 5\varepsilon\le \sum_{i<M}\sum_x\left|P_{b_i}(x)/M- \left(\sum_yq(y)P_y(x)\right)e_b(x,i)\right|}} \prod_{i<M}q(b_i) \le2K\exp\!\left(-\frac{\kappa\varepsilon^3}{\eta}\right).

No inclusion between $T_y$ and $T$ is assumed, and the sets may be empty when the other hypotheses permit it; $\varepsilon$ need not be less than $1$ .

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