Lemma 6: randomized conjugated projective measurement is gentle

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.lemma6_randomized_gentleness

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

prove2quantum

Let $\Lambda$ and $A$ be finite nonempty sets, $p$ a probability distribution, $V(\lambda)$ unitary, and $\{P_a\}_{a\in A}$ a complete family of self-adjoint orthogonal projectors, allowing zero projectors. Choose $\lambda$ , apply $V(\lambda)$ , measure, undo the same unitary, and discard the label. This defines

\mathcal G(\rho)=\sum_{\lambda,a}p(\lambda)V(\lambda)^\dagger P_aV(\lambda)\rho V(\lambda)^\dagger P_aV(\lambda).

For every density input, with $p_a(\rho)=\sum_\lambda p(\lambda)\operatorname{Tr}(P_aV(\lambda)\rho V(\lambda)^\dagger)$ ,

F(\rho,\mathcal G(\rho))\ge\max_{a\in A}p_a(\rho).

The maximum is attained. This is the randomized construction in H19–H21 for mixed states as well as pure states, rather than a hypothesis on an arbitrary channel.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P67

Formal statement

noncomputable section

open scoped ComplexConjugate Matrix Matrix.Norms.L2Operator

attribute [local instance] Classical.propDecidable

open MeasureTheory Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P67

variable {I J K L A : Type*} [Fintype I] [DecidableEq I]
  [Fintype J] [DecidableEq J] [Fintype K] [DecidableEq K]
  [Fintype L] [DecidableEq L] [Fintype A] [DecidableEq A]

/-- PDF pp.33–34, Lemma 6: the actual randomized conjugated measurement is gentle.
The expected probability has an attained maximum on the finite nonempty outcome type. -/
theorem lemma6_randomized_gentleness [Nonempty L] [Nonempty A]
    (p : L → ℝ) (hp : QAlgorithms.Learning.IsDistribution p) (V : L → Matrix.unitaryGroup I ℂ)
    (P : A → Matrix I I ℂ) (hP : ProjectiveFamily P) (rho : Matrix I I ℂ) (hrho : IsDensityMatrix rho) :
    (∃ a : A, ∀ b : A, gentleProbability p (fun l => (V l : Matrix I I ℂ)) P rho b ≤
      gentleProbability p (fun l => (V l : Matrix I I ℂ)) P rho a) ∧
    (∀ a : A, gentleProbability p (fun l => (V l : Matrix I I ℂ)) P rho a ≤
      rootFidelity rho (gentleChannel p (fun l => (V l : Matrix I I ℂ)) P rho)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 33, Lemma 6: randomized conjugated projective measurement is gentle

Read-back

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

Let $I,L,A$ be finite index types with decidable equality, with $L$ and $A$ nonempty. Let $p:L\to\mathbb R$ satisfy $p_l\ge0$ and $\sum_lp_l=1$ , let $V_l$ be a unitary matrix on $\mathbb C^I$ for every $l$ , and let $(P_a)_{a\in A}$ be Hermitian idempotent matrices satisfying $P_aP_b=0$ whenever $a\ne b$ and $\sum_aP_a=1$ . Let $\rho$ be positive semidefinite with trace $1$ . Define

q_a=\sum_l p_l\,\operatorname{Re}\operatorname{tr} (P_aV_l\rho V_l^\dagger), \qquad \Gamma=\sum_l p_l\sum_a (V_l^\dagger P_aV_l)\rho(V_l^\dagger P_aV_l)^\dagger.

There exists $a\in A$ such that $q_b\le q_a$ for every $b\in A$ , and, separately, every $a\in A$ satisfies

q_a\le \operatorname{Re}\operatorname{tr} \sqrt{\sqrt{\rho}\,\Gamma\,\sqrt{\rho}},

where square roots use continuous functional calculus. Zero probabilities and zero projectors are permitted; the density-matrix hypothesis cannot hold when $I$ is empty.

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