Geometric measure of entanglement of quantum state
import Quantum_state /-- Geometric measure of entanglment for pure states. 1 - max overlap with a 1-producible state More overlap means less of this measure -/ def gme_pure [quantum_state ψ] [pure ψ] : ℝ := 1 - max { |⟨φ|ψ⟩|² | 1_producible φ } /-- Geometric measure of entanglement for mixed states. -/ def gme [quantum_state ρ] : ℝ := Inf { ∑ i, (p i) * (gme_pure ψ i) | ∑ i, (p i) • (ψ i) = ρ }
The gme measures the distance to separable states.
/-- Uhlmann fidelity -/
def F(ρ, σ) := Tr√(√σ*ρ*√σ)
/-- gme in terms of the Uhlmann fidelity. -/
lemma gme_Uhlmann_fidelity_rw :
gme ρN = 1 − max { (F ρN σN)² | σN ∈ S₁N } :=
begin
sorry,
end
lemma gme_nonzero_of_tr_dist_to_separable_states_non_zero :
∀ c > 0,
min { trace_dist ρN σN | σN ∈ S₁N } ≥ c → gme ρN ≥ c² :=
begin
sorry,
end
/--
If a sequence {ρN} has vanishing gme
its elements must converge to the set of separable states
as N → ∞.
-/
lemma zero_tr_dist_to_separable_states_of_zero_gme :
lim gme ρN = 0 → lim min { trace_dist ρN σN | σN ∈ S₁N } = 0 :=
begin
sorry,
end