Prove2Me

(33), p. 7 — ψ ↦ ⟨φ|ψ⟩ is 1-Lipschitz: |⟨φ|ψ⟩ − ⟨φ|ψ′⟩| ≤ ‖ψ − ψ′‖₂

Proved
DirectFidelity.RandomState.eq_33

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

lipschitzp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1quantum-information

Let φ∈Cd\varphi \in \mathbb C^d be a state, ∥φ∥2=1\|\varphi\|_2 = 1. Then for all vectors ψ,ψ′∈Cd\psi, \psi' \in \mathbb C^d,

∣⟨φ∣ψ⟩−⟨φ∣ψ′⟩∣≤∥ψ−ψ′∥2.\bigl|\langle\varphi|\psi\rangle - \langle\varphi|\psi'\rangle\bigr| \le \|\psi - \psi'\|_2 .

That is, the overlap ψ↦⟨φ∣ψ⟩\psi \mapsto \langle \varphi|\psi\rangle is Lipschitz with coefficient η=1\eta = 1.

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

Formalization Note The inequality is stated for all vectors ψ,ψ′\psi,\psi', not only unit vectors; the paper uses it on the unit sphere, so this is a (harmless) generalisation.

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

open MeasureTheory

theorem eq_33 {n : ℕ} (φ : E n) (hφ : ‖φ‖ = 1) :
    ∀ ψ ψ' : E n, ‖inner ℂ φ ψ - inner ℂ φ ψ'‖ ≤ ‖ψ - ψ'‖ := by sorry
end DirectFidelity.RandomState
Source
Flammia and Liu, Direct fidelity estimation from few Pauli measurements, arXiv:1104.4695v3, p. 7, eq. (33)
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