Both limiting fractions of polarized split channels

Open

QAlgorithms.Papers.Independent.Intakethird100.P14.channel_polarization

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

prove2quantum

Let $W$ be any binary-input classical–quantum channel with normalized density outputs on a common complex Hilbert space. Its information $I(W)$ uses a uniform binary input and base-two logarithms. For $N=2^n$ , let $W_N^{(i)}$ be the actual split channels obtained by encoding with $G_N$ , exposing the previous bits as a classical register, and averaging the later bits uniformly. For every real $\delta\in(0,1)$ ,

\frac{\bigl|\{i:I(W_N^{(i)})\in(1-\delta,1]\}\bigr|}{N}\longrightarrow I(W),\qquad \frac{\bigl|\{i:I(W_N^{(i)})\in[0,\delta)\}\bigr|}{N}\longrightarrow1-I(W).

Both limits are taken as $n\to\infty$ . No symmetry, purity, finite-dimensionality, or strict inequality $0<I(W)<1$ is assumed. These fractions quantify the information carried by the polarized good and bad channels.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P14

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P14

open Filter MeasureTheory

open scoped ENNReal NNReal ComplexOrder BigOperators

open QAlgorithms.RealRegisters (Hilbert)

open QAlgorithms.Papers.Independent.Dependency50.P33 (IsDensity)

open QAlgorithms.Papers.Independent.Dependency50.P13 (compression)

open QAlgorithms.Papers.Independent.Renew46.P44 (wordOutput)

attribute [local instance] Classical.propDecidable Classical.decEq

/-- Theorem 2, PDF p.4; proof p.8. Both endpoint fractions, with exactly the
source's open and closed interval endpoints, converge along N=2^n. -/
theorem channel_polarization {I : Type} (W : Bit → OutputCoefficients I) (hW : IsBinaryCqChannel W)
    (delta : ℝ) (hd0 : 0 < delta) (hd1 : delta < 1) :
    Tendsto (fun n =>
      ((Finset.univ.filter (fun i : PolarWire n =>
        ENNReal.ofReal (1 - delta) < symmetricInformation (splitChannel W n i) ∧
        symmetricInformation (splitChannel W n i) ≤ 1)).card : ℝ≥0∞) / (2 ^ n : ℕ))
      atTop (nhds (symmetricInformation W)) ∧
    Tendsto (fun n =>
      ((Finset.univ.filter (fun i : PolarWire n =>
        0 ≤ symmetricInformation (splitChannel W n i) ∧
        symmetricInformation (splitChannel W n i) < ENNReal.ofReal delta)).card : ℝ≥0∞) /
          (2 ^ n : ℕ)) atTop (nhds (1 - symmetricInformation W)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P14

end

Source

Polar codes for classical-quantum channels, arXiv:1109.2591v3, PDF p. 4, Theorem 2 (Channel Polarization)

Read-back

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

For any type $I$ , let $W:\mathbb Z_2\to\mathbb C^{I\times I}$ have density arrays as outputs: each admits a countable expansion $W(b)_{ij}=\sum'_r u_r(i)\overline{v_r(j)}$ , with $u_r,v_r\in\ell^2(I;\mathbb C)$ and summable products $\|u_r\|\|v_r\|$ ; all its finite quadratic forms are real and nonnegative; and its real diagonal is summable with sum one. For any real $0<\delta<1$ , the assertion concerns the following split arrays. Put $N=2^n$ , let $b_k(r)$ denote bit $k$ , define $\operatorname{rev}_n(r)=(\sum_{k<n}b_k(r)2^{n-1-k})\bmod N$ , and put $G_{rt}=\prod_{k<n}K(b_k(\operatorname{rev}_n(r)),b_k(t))$ , with $K(a,0)=1,\ K(a,1)=a$ , over $\mathbb Z_2$ . For $i<N$ , define arrays on $\mathbb Z_2^i\times I^N$ by

V_i^{(n)}(b)_{(h,x),(h',y)} =\begin{cases} 2^{-(N-1)} \displaystyle\sum_{\substack{u\in\mathbb Z_2^N\\u_{<i}=h,\ u_i=b}} \prod_{t<N}W((uG)_t)_{x_t,y_t},&h=h',\\ 0,&h\ne h'. \end{cases}

For any binary array $V$ , set $\overline V=(V(0)+V(1))/2$ and $\mathcal I(V)=(D_2(V(0)\Vert\overline V)+D_2(V(1)\Vert\overline V))/2$ , where $D_2(X\Vert Y)$ is the supremum over every finite orthonormal family of the quantity

\begin{cases} \displaystyle\max\!\left\{0, \frac{\operatorname{Re}\operatorname{tr}(f(A)-A\log C-A+C)}{\log2}\right\}, &\ker C\subseteq\ker A,\\ \infty,&\text{otherwise}. \end{cases}

Here $A,C$ are the compressions of $O_X,O_Y$ to that family, $f(t)=t\log t$ , matrix functions use continuous functional calculus, and $O_X$ is a chosen bounded operator on the relevant complex $\ell^2$ space with coefficients $X$ , or zero if none exists. Then, in $[0,\infty]$ ,

\frac{\#\{i<2^n:1-\delta<\mathcal I(V_i^{(n)})\le1\}}{2^n} \longrightarrow\mathcal I(W), \qquad \frac{\#\{i<2^n:0\le\mathcal I(V_i^{(n)})<\delta\}}{2^n} \longrightarrow 1-\mathcal I(W).

The subtraction in the second limit is truncated subtraction in $[0,\infty]$ . The threshold inequalities are exactly the strict and non-strict inequalities displayed. The sequence includes $n=0$ , and no countability assumption on $I$ is imposed; empty $I$ makes the density hypothesis impossible.

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