Shared and private random data can be fixed

Open

QAlgorithms.Papers.Independent.Intakethird100.P11.randomness_canBeFixed

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

prove2quantum

Fix a finite normalized pure ensemble $\mathcal E=\{p_i,|v_i\rangle_{AB}\}$ in finite-dimensional complex Hilbert spaces, a positive blocklength $n$ , and positive compressed dimensions $d_A,d_B$ . Let $(\Omega,\mu)$ be a probability space for all input-independent random data, including the decoder's random data. For each seed $s\in\Omega$ , let $c_s$ consist of independent local CPTP encoders with these same output dimensions and a joint CPTP decoder. Define its ensemble-average squared fidelity by

F(c_s)=\sum_{i^n}\Bigl(\prod_{t=1}^np_{i_t}\Bigr) \langle v_{i^n}|c_s(|v_{i^n}\rangle\langle v_{i^n}|)|v_{i^n}\rangle, \qquad |v_{i^n}\rangle=\bigotimes_{t=1}^n|v_{i_t}\rangle.

If $s\mapsto F(c_s)$ is measurable, it is integrable and there is a seed $s_0$ such that

F(c_{s_0})\ge\int_\Omega F(c_s)\,d\mu(s).

Thus fixing all random data preserves the dimension budgets without reducing the randomized average fidelity. Applied at each blocklength, this removes shared or private randomness from the achievable-rate criterion.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P11

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P11

open MeasureTheory Filter

open scoped BigOperators ComplexConjugate Matrix

open QAlgorithms.Papers.Independent.Dependency50.P19 (both)

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

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF p.3, Section II: fixing every party's random data yields a valid deterministic
code with the same dimension budgets and fidelity at least its randomized average.
Measurability plus the normalized-source/channel bounds ensures genuine integrability. -/
theorem randomness_canBeFixed {I A B Omega : Type*}
    [Fintype I] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
    [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu]
    (p : I → ℝ) (hp : ∀ i, 0 ≤ p i) (htotal : ∑ i, p i = 1)
    (v : I → EuclideanSpace ℂ (A × B)) (hv : ∀ i, IsState (v i))
    (n da db : ℕ) (codes : Omega → DistributedBlockCode A B n da db)
    (hmeas : Measurable (fun seed => finiteFidelity p v (codes seed))) :
    Integrable (fun seed => finiteFidelity p v (codes seed)) mu ∧
      ∃ seed, (∫ s, finiteFidelity p v (codes s) ∂mu) ≤ finiteFidelity p v (codes seed) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P11

end

Source

On the distributed compression of quantum information, arXiv:quant-ph/0403042v3, PDF p. 3, Section II: shared and private randomness can be fixed

Read-back

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

Let $I,A,B$ be finite types, with decidable equality on $A,B$ , and let $\Omega$ be a measurable space equipped with a probability measure $\mu$ . Let $p:I\to\mathbb R$ satisfy $p_i\ge0$ for every $i$ and $\sum_i p_i=1$ , and let $v_i\in\mathbb C^{A\times B}$ have Euclidean norm $1$ for every $i$ , including labels of weight zero. Fix natural numbers $n,d_A,d_B$ and, for every seed $s\in\Omega$ , a distributed block code $C_s$ . Each code includes the requirements $n,d_A,d_B>0$ , encoding channels $E_{A,s}$ and $E_{B,s}$ from the respective $n$ -letter registers to dimensions $d_A,d_B$ , and a decoding channel $D_s$ back to the two $n$ -letter registers. Here a channel is a map admitting a finite representation $X\mapsto\sum_j K_jXK_j^\dagger$ with $\sum_jK_j^\dagger K_j=1$ . Write $\mathcal C_s=D_s\circ(E_{A,s}\otimes E_{B,s})$ , where the two encoders act separately on their registers. For $w:\{0,\ldots,n-1\}\to I$ , define $V_w(a,b)=\prod_{t=0}^{n-1}v_{w(t)}(a_t,b_t)$ , $P_w=V_wV_w^\dagger$ , and

F(s)=\sum_w\left(\prod_{t=0}^{n-1}p_{w(t)}\right) \operatorname{Re}\operatorname{tr}\!\left(P_w\,\mathcal C_s(P_w)\right).

If the real function $F$ is measurable, then it is integrable with respect to $\mu$ , and there exists a seed $s\in\Omega$ such that $\int_\Omega F\,d\mu\le F(s)$ . The normalization assumptions exclude empty $I,A,B$ ; no measurability of the code assignment itself is assumed beyond measurability of $F$ .

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