Generalized quantum Stein lemma

A source makes ρ or σ.

We want to know which.

We can ask the source to make arbitrarily many copies.

For n systems: ρ^⊗n or σ^⊗n.

But what if the source output depends on previous outputs?

So instead of σ^⊗n the source makes ωₙ..

  • Generalize the σ^⊗n in the original Quantum Stein lemma to an arbitary state ωₙ.

    • If the null hypothesis is an ergodic state, instead of i.i.d.

    • If the null and alternative hypotheses are correlated states.

    • If the alternative hypothesis is an arbitrary state. If the source

import POVM
import Quantum_relative_entropy 

import Permutation_group

variables (ℋ : Type) [complex_Hilbert_space ℋ]
(ρ : ℋ →ₗ[ℂ] ℋ) [quantum_state ρ]

class arbitrary_states (μ : Π n : ℕ, set ℋ^⊗n →ₗ[ℂ] ℋ^⊗n) :=
(quantum_states : ∀ n, ∀ ωₙ ∈ μ n, quantum_state ωₙ)
(convex_μₙ : ∀ n, convex μ n)
(closed_μₙ : ∀ n, closed μ n)
(contains_full_rank_state : ∀ n, ∃ [quantum_state σ] [full_rank σ], σ^⊗n ∈ μ n)
(closed_under_perm : ∀ n, ∀ π ∈ Sₙ, (P π) ρ (P π) ∈ ℳ n)
(closed_under_ptrace : ∀ n, ∀ ρ ∈ ℳ(n+1), ∀ k ∈ {1,...,n+1}, trₖ(ρ) ∈ ℳ n)
(closed_under_tensor_products : ∀ n m, ∀ ρ ∈ ℳ n, ∀ ν ∈ ℳ m, ρ ⊗ ν ∈ ℳ(n + m))

/-
An example of such set is S(ℋ^⊗n)
the set of k-partite separable states
over ℋ^⊗n := ℋ₁^⊗n ⊗ ... ⊗ ℋₖ^⊗n.
-/

variables 
(μ : Π n : ℕ, set ℋ^⊗n →ₗ[ℂ] ℋ^⊗n) [∀ n, arbitrary_states (μ n)]

variable (n : ℕ)

/-- Hypothesis test. Instance of POVM -/
def test (Aₙ : (ℋ^⊗n) →ₗ[ℂ] (ℋ^⊗n)) :=
0 ≤ Aₙ ∧ Aₙ ≤ 1 

variables (Aₙ : ℋ^⊗n →ₗ[ℂ] ℋ^⊗n) [test Aₙ]

/-- inf "distance" to states in ℳ -/
def Eℳ(ρ) := inf { quantum_relative_entropy ρ σ | σ ∈ ℳ }

/-- Eℳ∞(ρ) is the number at the end of the sequence. -/
def Eℳ∞(ρ) := lim λ n, Eℳ(ρ^⊗n)/n

/-- "Regularized relative entropy of entanglement" -/
def ER∞(ρ) := lim λ n, 1/n * min{quantum_relative_entropy ρ^⊗n σ | σ ∈ S(ℋ^⊗n)}

/-- Probability of guessing ρ^⊗n when actually ωₙ. -/
def α Aₙ := tr(Aₙ * ωₙ)

/-- Probability of guessing σ^⊗n when actually ρ^⊗n. -/
def β := tr(ρ^⊗n * (1 - Aₙ))

/-- What is the minimum? -/
def min_α_if_β_leq_ε (ε > 0) := 
- log min { α Aₙ | Aₙ : ℋ^⊗n →ₗ[ℂ] ℋ^⊗n ∧ test Aₙ ∧ β Aₙ < ε }

/--
General quantum Stein lemma.

This is theorem 1 here:
https://arxiv.org/abs/0904.0281v3.
-/
theorem theorem1_direct_part :
∀ε>0,
∃ (Aₙ : ℕ → (ℋ^⊗n →ₗ[ℂ] ℋ^⊗n)) [∀ n, test Aₙ n],
lim λ n, β Aₙ = 0
∧
∀n, ∀ ωₙ ∈ ℳ n, - log α Aₙ / n + ε ≥ Eℳ∞(ρ)

/--
If α > Eℳ∞ then
"not only does β not go to zero
but it actually goes to one."
-/
theorem theorem1_strong_converse (ε > 0) (Aₙ : ℕ → (ℋ^⊗n →ₗ[ℂ] ℋ^⊗n)) [∀ n, test Aₙ n] : 
∀n, ∀ ωₙ ∈ ℳ n, - log α Aₙ / n - ε ≥ Eℳ∞(ρ)
→
lim λ n, β Aₙ = 1 :=
begin
  sorry,
end

-- other possible phrasings

theorem theorem1_direct' :
∀ ε > 0, ∀ δ > 0,
∃ k : ℕ, ∀ n > k,
∃ (Aₙ : ℋ^⊗n →ₗ[ℂ] ℋ^⊗n) [test Aₙ],
∀ ωₙ ∈ ℳ n,
β Aₙ < ε
∧
- log α Aₙ / n ≥ E∞ℳ(ρ) - δ :=
begin
  sorry,
end

theorem theorem1_direct'' :
∀ ε > 0, ∀ δ > 0,
∃ k : ℕ, ∀ n > k,
∀ ωₙ ∈ ℳ n,
- log min_α_if_β_leq_ε n ε / n > E∞ℳ(ρ) - δ :=
begin
  sorry,
end

/-- Compare with the statement of the original quantum Stein lemma. -/
lemma log_minimum_tends_to_quantum_relative_entropy_for_sufficiently_many_systems : 
∀ ε > 0,
lim λ n, log min_α_if_β_leq_ε n ε / n = - E∞ℳ(ρ) :=
begin
  -- follows from the stuff above
  splitting_tactic_here,
  sorry,
end

Would be nice to prove because “implies whenever a multipartite state can be asymptotically converted into another entangled state by local operations and classical communication, the rate of conversion must be non-zero.”

lemma propIII1a {y : ℝ} : 
y > Eℳ∞(ρ) → lim λ n, min{tr(ρ^⊗n - 2^{yn} * ωₙ) | ωₙ ∈ ℳ n} = 0 :=
begin
  sorry,
end

lemma propIII1b {y : ℝ} : 
y < Eℳ∞(ρ) → lim λ n, min{tr(ρ^⊗n - 2^{yn} * ωₙ) | ωₙ ∈ ℳ n} = 1 :=
begin
  sorry,
end

def tr₊(A) := min{tr Y | Y ≥ A ∧ Y ≥ 0}

/-- Family of convex optimization problems -/
def γ {n : ℕ} (π : quantum_state) (K : ℝ) :=
max {tr(A π) | test Aₙ ∧ ∀ σ ∈ ℳ n, tr(A σ) ≤ 1/K}

/- propIII1 -> theorem1 -/
The statement of theorem1 is implied by

y > Eℳ∞(ρ) → lim λ n, γ ρ^⊗n 2^{yn} = 0

y < Eℳ∞(ρ) → lim λ n, γ ρ^⊗n 2^{yn} = 1.

In order to see that this holds true:

Show the problem is equal to its dual formulation

From propIII1 we find
lim λ n, γ ρ^⊗n 2^{yn} = 0.

And from another simple argument we find
lim λ n, γ ρ^⊗n 2^{yn} = 1.

/-
Equation 122:
ωₙ := 1/(1+τ) ωₙ' + τ/(1+τ) * σ^⊗(n-m-r)
-/
variables
[τ > 0]
[ωₙ ...]

/-
Equation 115:
πₙ := tr₁ tr₂ ... trᵣ trₑ (|Φ⟩⟨Φ| / ⟨φ|φ⟩)
-/
variables
[πₙ ...]

variables
[ν > 0]
[λ = λnν ≥ quantum_relative_entropy(πₙ, ωₙ) + ν*n]

lemma III9 :
∃ γ > 0,
∃ (l : ℕ → (ℋ →ₗ[ℂ] ℋ)) [∀ i, quantum_state l i],
∃ n, ∀ k > n,
∃ [quantum_state l] ≥ (l k),
tr(πₙ⊗l - 2^{λnν} * ωₙ⊗l)+ ≤ 2^{-γ*n*l} :=
begin
  sorry,
end

References