Appendix F, Eqs.(F1)–(F5): reflection and unitary perturbation estimates

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.reflection_perturbation

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

prove2quantum

Let two normalized pure sample families $\phi_k,\widetilde\phi_k$ satisfy $|\langle\phi_k|\widetilde\phi_k\rangle|^2\ge1-\delta^2$ , $\delta\ge0$ . For $R_\phi=I-2\lvert\phi\rangle\langle\phi\rvert$ and the corresponding controlled reflections and $W(k)=R(k)HR(a)$ ,

\|R_\phi-R_{\widetilde\phi}\|_\infty=2\sqrt{1-|\langle\phi|\widetilde\phi\rangle|^2},\quad\|R^c_k-\widetilde R^c_k\|_\infty\le2\delta,\quad\|W(k)-\widetilde W(k)\|_\infty\le4\delta.

For arbitrary pairs of unitary factors, the norm of the difference of their two-factor products is at most the sum of the two factor differences. For every density operator $\sigma$ and unitaries $V,\widetilde V$ ,

\tfrac12\|V\sigma V^\dagger-\widetilde V\sigma\widetilde V^\dagger\|_1\le\|V-\widetilde V\|_\infty.

The analogous distance for finite probability mixtures is at most the corresponding average of operator-norm differences. These are F1–F5, independent of how a consumed output-anchor resource is changed.

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 p.27, F1–F5: all algebraic perturbation estimates, without claiming Eq.(33)
for changed consumed-anchor resources. -/
theorem reflection_perturbation [Nonempty L] (phi phitilde : K → EuclideanSpace ℂ I) (a : K)
    (hphi : ∀ k, IsState (phi k)) (htilde : ∀ k, IsState (phitilde k))
    (delta : ℝ) (hdelta : 0 ≤ delta)
    (hoverlap : ∀ k, 1 - delta ^ 2 ≤ ‖inner ℂ (phi k) (phitilde k)‖ ^ 2) :
    (∀ k, QAlgorithms.specNorm (sampleReflection (phi k) - sampleReflection (phitilde k)) =
      2 * Real.sqrt (1 - ‖inner ℂ (phi k) (phitilde k)‖ ^ 2)) ∧
    (∀ k, QAlgorithms.specNorm (systemControlled (sampleReflection (phi k)) - systemControlled (sampleReflection (phitilde k))) ≤ 2 * delta) ∧
    (∀ k, QAlgorithms.specNorm (erasureGate phi a k - erasureGate phitilde a k) ≤ 4 * delta) ∧
    (∀ V1 V2 W1 W2 : Matrix.unitaryGroup I ℂ,
      QAlgorithms.specNorm ((W2 : Matrix I I ℂ) * (W1 : Matrix I I ℂ) - (V2 : Matrix I I ℂ) * (V1 : Matrix I I ℂ)) ≤
        QAlgorithms.specNorm ((W2 : Matrix I I ℂ) - (V2 : Matrix I I ℂ)) + QAlgorithms.specNorm ((W1 : Matrix I I ℂ) - (V1 : Matrix I I ℂ))) ∧
    (∀ rho : Matrix I I ℂ, IsDensityMatrix rho → ∀ V W : Matrix.unitaryGroup I ℂ,
      traceDistance (densityConjugation (V : Matrix I I ℂ) rho) (densityConjugation (W : Matrix I I ℂ) rho) ≤
        QAlgorithms.specNorm ((V : Matrix I I ℂ) - (W : Matrix I I ℂ))) ∧
    (∀ rho : Matrix I I ℂ, IsDensityMatrix rho → ∀ p : L → ℝ, QAlgorithms.Learning.IsDistribution p →
      ∀ V W : L → Matrix.unitaryGroup I ℂ,
      traceDistance (∑ l, (p l : ℂ) • densityConjugation (V l : Matrix I I ℂ) rho)
        (∑ l, (p l : ℂ) • densityConjugation (W l : Matrix I I ℂ) rho) ≤
        ∑ l, p l * QAlgorithms.specNorm ((V l : Matrix I I ℂ) - (W l : Matrix I I ℂ))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 27, Appendix F, Eqs.(F1)–(F5): reflection and unitary perturbation estimates

Read-back

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

Let $I,K,L$ be finite index types with decidable equality, with $L$ nonempty, fix $a\in K$ , and let $\phi_k,\widetilde\phi_k\in\mathbb C^I$ have norm $1$ for every $k\in K$ . Let $\delta\ge0$ , with no upper bound imposed, and assume $1-\delta^2\le|\langle\phi_k,\widetilde\phi_k\rangle|^2$ for every $k$ . Define $R_k=1-2\phi_k\phi_k^\dagger$ , $\widetilde R_k=1-2\widetilde\phi_k\widetilde\phi_k^\dagger$ , $C(V)=1_I\otimes|0\rangle\langle0|+V\otimes|1\rangle\langle1|$ , $H=2^{-1/2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}$ , $E_k=C(R_k)(1_I\otimes H)C(R_a)$ , and $\widetilde E_k=C(\widetilde R_k)(1_I\otimes H)C(\widetilde R_a)$ . Write $\|\cdot\|_{\mathrm{op}}$ for the Euclidean operator norm and $D(A,B)=\frac12\operatorname{Re}\operatorname{tr}\sqrt{(A-B)^\dagger(A-B)}$ , using functional calculus for the square root. The assertion is the conjunction of the following statements: for every $k$ ,

\|R_k-\widetilde R_k\|_{\mathrm{op}} =2\sqrt{1-|\langle\phi_k,\widetilde\phi_k\rangle|^2}, \qquad \|C(R_k)-C(\widetilde R_k)\|_{\mathrm{op}}\le2\delta, \qquad \|E_k-\widetilde E_k\|_{\mathrm{op}}\le4\delta;

for every four unitary matrices $V_1,V_2,W_1,W_2$ on $\mathbb C^I$ ,

\|W_2W_1-V_2V_1\|_{\mathrm{op}} \le\|W_2-V_2\|_{\mathrm{op}}+\|W_1-V_1\|_{\mathrm{op}};

for every positive semidefinite matrix $\rho$ of trace $1$ and every two unitary matrices $V,W$ ,

D(V\rho V^\dagger,W\rho W^\dagger)\le\|V-W\|_{\mathrm{op}};

and for every such $\rho$ , every function $p:L\to\mathbb R$ satisfying $p_l\ge0$ and $\sum_lp_l=1$ , and every two unitary-valued families $V_l,W_l$ ,

D\!\left(\sum_lp_lV_l\rho V_l^\dagger,\sum_lp_lW_l\rho W_l^\dagger\right) \le\sum_lp_l\|V_l-W_l\|_{\mathrm{op}}.

No lower bound on $|K|$ beyond the existence of $a$ is assumed.

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