All local and cumulative information and fidelity identities

Open

QAlgorithms.Papers.Independent.Intakethird100.P14.all_transformation_identities

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. For $N=2^n$ , $n\ge0$ , write $I_i=I(W_N^{(i)})$ and $f_i=\sqrt{F(W_N^{(i)})}$ , where information uses the uniform prior and bits, and $F$ is squared fidelity. Write $I_{i,-},f_{i,-}$ and $I_{i,+},f_{i,+}$ for the corresponding quantities of children $W_{2N}^{(2i-1)}$ and $W_{2N}^{(2i)}$ . For every $1\le i\le N$ ,

I_{i,-}+I_{i,+}=2I_i,\qquad f_{i,-}+f_{i,+}\le2f_i,

I_{i,-}\le I_i\le I_{i,+},\qquad f_{i,-}\ge f_i\ge f_{i,+},

f_{i,+}=F(W_N^{(i)}),\qquad f_{i,-}\le2f_i-F(W_N^{(i)}).

The cumulative quantities also satisfy

\sum_{i=1}^N I_i=NI(W),\qquad \sum_{i=1}^N f_i\le N\sqrt{F(W)}.

This states the entire proposition through (29), including both unnumbered ordering displays. It propagates the single-step transform to every level of the actual channel tree.

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

/-- Proposition 10, PDF p.8: every local assertion (24)–(27), both
unnumbered ordering displays, and cumulative (28)–(29). -/
theorem all_transformation_identities {I : Type} (W : Bit → OutputCoefficients I) (hW : IsBinaryCqChannel W)
    (n : ℕ) :
    (∀ i : PolarWire n,
      symmetricInformation (splitChannel W (n + 1) (childIndex i false)) +
        symmetricInformation (splitChannel W (n + 1) (childIndex i true)) =
          2 * symmetricInformation (splitChannel W n i) ∧
      Real.sqrt (squaredCqFidelity (splitChannel W (n + 1) (childIndex i false))) +
        Real.sqrt (squaredCqFidelity (splitChannel W (n + 1) (childIndex i true))) ≤
          2 * Real.sqrt (squaredCqFidelity (splitChannel W n i)) ∧
      symmetricInformation (splitChannel W (n + 1) (childIndex i false)) ≤
        symmetricInformation (splitChannel W n i) ∧
      symmetricInformation (splitChannel W n i) ≤
        symmetricInformation (splitChannel W (n + 1) (childIndex i true)) ∧
      Real.sqrt (squaredCqFidelity (splitChannel W n i)) ≤
        Real.sqrt (squaredCqFidelity (splitChannel W (n + 1) (childIndex i false))) ∧
      Real.sqrt (squaredCqFidelity (splitChannel W (n + 1) (childIndex i true))) ≤
        Real.sqrt (squaredCqFidelity (splitChannel W n i)) ∧
      Real.sqrt (squaredCqFidelity (splitChannel W (n + 1) (childIndex i true))) =
        squaredCqFidelity (splitChannel W n i) ∧
      Real.sqrt (squaredCqFidelity (splitChannel W (n + 1) (childIndex i false))) ≤
        2 * Real.sqrt (squaredCqFidelity (splitChannel W n i)) - squaredCqFidelity (splitChannel W n i)) ∧
    (∑ i : PolarWire n, symmetricInformation (splitChannel W n i)) =
      (2 ^ n : ℕ) * symmetricInformation W ∧
    (∑ i : PolarWire n, Real.sqrt (squaredCqFidelity (splitChannel W n i))) ≤
      (2 ^ n : ℕ) * Real.sqrt (squaredCqFidelity W) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P14

end

Source

Polar codes for classical-quantum channels, arXiv:1109.2591v3, PDF p. 8, Proposition 10: all local and cumulative transformation identities (24)–(29)

Read-back

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

Let $I$ be any type and $W_0,W_1$ density coefficient arrays on $\ell^2(I;\mathbb C)$ , meaning that each has an expansion $X(a,b)=\sum_r u_r(a)\overline{v_r(b)}$ with $\sum_r\|u_r\|\|v_r\|<\infty$ , real nonnegative finite quadratic forms, and summable real diagonal of sum $1$ . For any array $X$ , let $O(X)$ be a chosen bounded operator with coefficients $X$ , or $0$ if none exists; let $R(T)$ be a chosen positive bounded square root of $T$ , or $0$ if none exists; and put $\operatorname{tr}_bT=\sum_j(Te_j)_j$ , with nonsummable families assigned total sum $0$ . Define $F(V)=[\operatorname{Re}\operatorname{tr}_bR(R(O(V_0))O(V_1)R(O(V_0)))]^2$ , and $Z(V)=\sqrt{F(V)}$ . Define $D_2(X\mid Y)$ as the supremum over $d\ge0$ and orthonormal $d$ -tuples $v$ of $+\infty$ when $\ker Y_v\not\subseteq\ker X_v$ , and otherwise of $\max(0,\operatorname{Re}\operatorname{Tr}(f(X_v)-X_v\log Y_v-X_v+Y_v)/\log2)$ , where $X_v=(\langle v_r,O(X)v_s\rangle)$ , $Y_v=(\langle v_r,O(Y)v_s\rangle)$ , $f(t)=t\log t$ , and matrix functions use continuous functional calculus. Put $J(V)=\tfrac12[D_2(V_0\mid(V_0+V_1)/2)+D_2(V_1\mid(V_0+V_1)/2)]$ . For $n\ge0$ , put $N=2^n$ and $G_n(r,c)=\prod_{k<n}\kappa(\operatorname{bit}_k(\operatorname{rev}_n r),\operatorname{bit}_k(c))$ , where $\kappa(a,0)=1,\ \kappa(a,1)=a$ , and $\operatorname{rev}_n$ reverses $n$ bits. For $u\in\mathbb F_2^N$ , set $V_u(y,z)=\prod_{c<N}W_{\sum_r u_rG_n(r,c)}(y_c,z_c)$ . For $i<N$ , a prefix $h\in\mathbb F_2^i$ , and bit $b$ , set $T_{n,i,h,b}=2^{-N}\sum_{v\in\mathbb F_2^N}V_{\operatorname{fill}(h,b,v)}$ , where the filled word uses $h$ before $i$ , $b$ at $i$ , and $v$ afterward; define $W_{n,i}^b((h,y),(h',z))=\mathbf1_{h=h'}2^{-i}T_{n,i,h,b}(y,z)$ . Then, for every $n\in\mathbb N$ and every $i<2^n$ , writing $V=W_{n,i}$ , $V^-=W_{n+1,2i}$ , and $V^+=W_{n+1,2i+1}$ , all eight assertions hold:

\begin{gathered} J(V^-)+J(V^+)=2J(V),\qquad Z(V^-)+Z(V^+)\le2Z(V),\\ J(V^-)\le J(V),\qquad J(V)\le J(V^+),\\ Z(V)\le Z(V^-),\qquad Z(V^+)\le Z(V),\\ Z(V^+)=F(V),\qquad Z(V^-)\le2Z(V)-F(V). \end{gathered}

Moreover,

\sum_{i<2^n}J(W_{n,i})=2^nJ(W), \qquad \sum_{i<2^n}Z(W_{n,i})\le2^nZ(W).

The information quantities and their sums are extended nonnegative reals, whereas the $Z$ -quantities and their sums are real. The statement includes $n=0$ , with one index, empty bit products, and empty prefixes.

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