Prove2Me

(36), p. 7 — on unit vectors ψ ↦ ⟨ψ|W_k|ψ⟩ is 2-Lipschitz

Proved
DirectFidelity.RandomState.eq_36

by mikedeng1 · Oct 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

lipschitzp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1pauli-operatorsquantum-information

Let WkW_k be an nn-qubit Pauli operator and let ψ,ψ′∈Cd\psi, \psi' \in \mathbb C^d be unit vectors. Then

∣⟨ψ∣Wk∣ψ⟩−⟨ψ′∣Wk∣ψ′⟩∣≤∣⟨ψ∣Wk[∣ψ⟩−∣ψ′⟩]∣+∣[⟨ψ∣−⟨ψ′∣]Wk∣ψ′⟩∣≤2∥ψ−ψ′∥2.\bigl|\langle\psi|W_k|\psi\rangle - \langle\psi'|W_k|\psi'\rangle\bigr| \le \bigl|\langle\psi|W_k\bigl[|\psi\rangle - |\psi'\rangle\bigr]\bigr| + \bigl|\bigl[\langle\psi| - \langle\psi'|\bigr]W_k|\psi'\rangle\bigr| \le 2\|\psi - \psi'\|_2 .

So on the unit sphere the Pauli expectation is Lipschitz with coefficient η=2\eta = 2.

This is the Lipschitz estimate that feeds Levy's lemma in (37).

Formalization Note Both inequalities of the printed chain are stated. The unit-norm hypotheses on ψ,ψ′\psi, \psi' are the paper's (they are points of the sphere) and are needed, since the map is quadratic.

Preamble
import Mathlib
import Definitions.Def_DirectFidelity_RandomState_Setting
Formal statement
namespace DirectFidelity.RandomState

open MeasureTheory

theorem eq_36 {n : ℕ} (k : DirectFidelity.State.P n) (ψ ψ' : E n) (hψ : ‖ψ‖ = 1) (hψ' : ‖ψ'‖ = 1) :
    ‖pauliExp k ψ - pauliExp k ψ'‖ ≤
        ‖inner ℂ ψ (Matrix.toEuclideanLin (DirectFidelity.State.W k) (ψ - ψ'))‖ +
          ‖inner ℂ (ψ - ψ') (Matrix.toEuclideanLin (DirectFidelity.State.W k) ψ')‖ ∧
      ‖inner ℂ ψ (Matrix.toEuclideanLin (DirectFidelity.State.W k) (ψ - ψ'))‖ +
          ‖inner ℂ (ψ - ψ') (Matrix.toEuclideanLin (DirectFidelity.State.W k) ψ')‖ ≤ 2 * ‖ψ - ψ'‖ := by sorry
end DirectFidelity.RandomState
Source
Flammia and Liu, Direct fidelity estimation from few Pauli measurements, arXiv:1104.4695v3, p. 7, eq. (36)
Human review

  • Endorsed by Shuze Chen · Oct 15, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 15, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph