Forward rate of polarization: small sum of root fidelities

Open

QAlgorithms.Papers.Independent.Intakethird100.P14.rate_of_polarization_forward

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

prove2quantum

Let $W$ be a binary-input classical–quantum channel with normalized density outputs and uniform-prior Holevo information $I(W)>0$ , in bits. Fix real constants $R<I(W)$ and $\beta<1/2$ . For every $N=2^n$ , form the split channels $W_N^{(i)}$ using the actual polar encoder, the exposed classical history, and uniform future bits. There exists a sequence of information sets $A_N\subseteq\{1,\ldots,N\}$ such that

|A_N|\ge NR\quad\hbox{for every }n\ge0,\qquad \sum_{i\in A_N}\sqrt{F(W_N^{(i)})}=o\!\left(2^{-N^\beta}\right).

Here $F$ is squared fidelity and the asymptotic limit is $n\to\infty$ . The sum, rather than its average or maximum, is controlled. The source allows negative $R$ and negative $\beta$ ; for negative $R$ the empty information set is admissible. This assertion supplies the reliability input for the coding theorem.

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 3, forward clause, PDF p.5; proof p.9. The quantity is a SUM,
not an average or maximum. Negative R and beta are allowed as printed.
The cardinality condition holds at every blocklength, including N=1. -/
theorem rate_of_polarization_forward {I : Type} (W : Bit → OutputCoefficients I) (hW : IsBinaryCqChannel W)
    (hI : 0 < symmetricInformation W) (R beta : ℝ)
    (hR : ENNReal.ofReal R < symmetricInformation W) (hb : beta < 1 / 2) :
    ∃ A : (n : ℕ) → Finset (PolarWire n),
      (∀ n, (2 ^ n : ℕ) * R ≤ ((A n).card : ℝ)) ∧
      Asymptotics.IsLittleO atTop
        (fun n => ∑ i ∈ A n, Real.sqrt (squaredCqFidelity (splitChannel W n i)))
        (polarDecay beta 1) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P14

end

Source

Polar codes for classical-quantum channels, arXiv:1109.2591v3, PDF p. 5, Theorem 3 (Rate of Polarization), forward assertion

Read-back

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

For any type $I$ , suppose $W:\mathbb Z_2\to\mathbb C^{I\times I}$ has density outputs: each $W(b)$ has 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 an array $X$ , let $O_X$ be a chosen bounded operator with coefficients $X$ , or zero if none exists. Define $D_2(X\Vert Y)$ as the supremum over all finite orthonormal families, including the empty family, of

\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}

where $A,C$ compress $O_X,O_Y$ to the family, $f(t)=t\log t$ , and matrix functions use continuous functional calculus. Put $\overline W=(W(0)+W(1))/2$ and $\mathcal I(W)=(D_2(W(0)\Vert\overline W)+D_2(W(1)\Vert\overline W))/2$ . Assume $\mathcal I(W)>0$ , and let $R,\beta\in\mathbb R$ satisfy $\max\{R,0\}<\mathcal I(W)$ and $\beta<\tfrac12$ . For $N=2^n$ , define the bit-reversal integer $\operatorname{rev}_n(r)=(\sum_{k<n}b_k(r)2^{n-1-k})\bmod N$ , where $b_k(r)$ is bit $k$ , and the matrix $G_{rt}=\prod_{k<n}K(b_k(\operatorname{rev}_n(r)),b_k(t))$ over $\mathbb Z_2$ , with $K(a,0)=1,\ K(a,1)=a$ . Define split arrays, indexed by $(h,x)\in\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 a binary array $V$ , let

F(V)=\left(\operatorname{Re}\sum'_x \left[R\!\left(R(O_{V(0)})O_{V(1)}R(O_{V(0)})\right)e_x\right]_x\right)^2,

where $R(T)$ is a chosen positive bounded square root of $T$ , or zero if none exists; a nonsummable complex sum is zero. There exist subsets $A_n\subseteq\{0,\ldots,2^n-1\}$ such that, for every $n$ , $2^nR\le|A_n|$ , and

\sum_{i\in A_n}\sqrt{F(V_i^{(n)})} =o\!\left(2^{-(2^n)^\beta}\right)\qquad(n\to\infty).

Equivalently, for every $c>0$ , the sum is eventually at most $c\,2^{-(2^n)^\beta}$ . No nonnegativity requirement is imposed on $R$ or $\beta$ ; when $R<0$ , the cardinality bound is automatic. The case $n=0$ is included, and no countability assumption on $I$ is present.

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