def MState.fidelity {d : Type u_1} [Fintype d] (ρ σ : MState d) : ℝ

The fidelity of two quantum states. This is the quantum version of the Bhattacharyya coefficient.

Equations

• ρ.fidelity σ = ⋯.rtrace ^ 2

theorem MState.fidelity_ge_zero {d : Type u_1} [Fintype d] (ρ σ : MState d) : 0 ≤ ρ.fidelity σ

theorem MState.fidelity_le_one {d : Type u_1} [Fintype d] (ρ σ : MState d) : ρ.fidelity σ ≤ 1

def MState.fidelity_prob {d : Type u_1} [Fintype d] (ρ σ : MState d) : Prob

The fidelity, as a Prob probability with value between 0 and 1.

Equations

• ρ.fidelity_prob σ = ⟨ρ.fidelity σ, ⋯⟩

theorem MState.fidelity_self_eq_one {d : Type u_1} [Fintype d] (ρ : MState d) : ρ.fidelity ρ = 1

A state has perfect fidelity with itself.

theorem MState.fidelity_eq_one_iff_self {d : Type u_1} [Fintype d] (ρ σ : MState d) : ρ.fidelity σ = 1 ↔ ρ = σ

The fidelity is 1 if and only if the two states are the same.

theorem MState.fidelity_symm {d : Type u_1} [Fintype d] (ρ σ : MState d) : ρ.fidelity σ = σ.fidelity ρ

The fidelity is a symmetric quantity.

theorem MState.fidelity_channel_nondecreasing {d : Type u_1} {d₂ : Type u_2} [Fintype d] [Fintype d₂] (ρ σ : MState d) (Λ : CPTPMap d d₂) : (Λ ρ).fidelity (Λ σ) ≥ ρ.fidelity σ

The fidelity cannot decrease under the application of a channel.