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.
Distinguish probability distributions;
Use a two-element POVM {Aₙ, 1-Aₙ};
import POVM import Quantum_relative_entropy import order.liminf_limsup import topology.sequences variables (ℋ : Type) [complex_Hilbert_space ℋ] variables {ρ : ℋ →ₗ[ℂ] ℋ} [quantum_state ρ] {σ : ℋ →ₗ[ℂ] ℋ} [quantum_state σ] variable (n : ℕ) /-- Hypothesis test. Instance of POVM. -/ def test (Aₙ : ℋ^⊗n →ₗ[ℂ] ℋ^⊗n) := 0 ≤ Aₙ ∧ Aₙ ≤ 1 variables (Aₙ : ℋ^⊗n →ₗ[ℂ] ℋ^⊗n) [test Aₙ] /-- Probability of guessing σ^⊗n when actually ρ^⊗n -/ def α := tr(ρ^⊗n * (1 - Aₙ)) /-- Probability of guessing ρ^⊗n when actually σ^⊗n -/ def β := tr(σ^⊗n * Aₙ) /-- What is the minimum? -/ def min_β_if_α_leq_ε (ε > 0) := min {β Aₙ | Aₙ : ℋ^⊗n →ₗ[ℂ] ℋ^⊗n ∧ test Aₙ ∧ α Aₙ ≤ ε} /-- "Hiai and Petz showed" -/ lemma limsup_log_min_β_if_α_leq_ε_leq_neg_rel_entropy (ε > 0) : limsup λ n, log min_β_if_α_leq_ε ε / n ≤ - quantum_relative_entropy ρ σ := begin sorry, end
variables
{r : ℝ}
(μₙ : ι → ℝ)
(Eₙ : ι → (ℋ^⊗n →ₗ[ℂ] ℋ^⊗n))
[∑ j, (μₙ j) * (Eₙ j) = ρ^⊗n - exp(n*r) * σ^⊗n]
def Dₙ := {j : ι | μₙ j ≥ 0}
def Xₙr := ∑ j ∈ Dₙ, (Eₙ j)
lemma lemma1 {Aₙ : ℋ^⊗n →ₗ[ℂ] ℋ^⊗n} [test Aₙ] :
tr(ρ^⊗n - exp(n*r) * σ^⊗n) * Xₙr ≥ tr(ρ^⊗n - exp(n*r) * σ^⊗n) * Aₙ :=
begin
calc tr(ρ^⊗n - exp(n*r) * σ^⊗n) * Aₙ = ∑ j, (μₙ j) * tr(Eₙ j Aₙ)
... ≤ ∑ j ∈ Dₙ, (μₙ j) * tr(Eₙ j Aₙ) : by sorry,
... ≤ ∑ j ∈ Dₙ, (μₙ j) * tr(Eₙ j) : by sorry,
... = tr(ρ^⊗n - exp(n*r) * σ^⊗n) * Xₙr : by sorry,
sorry,
end
/--
ψ(0) = 0
d/ds ψ(s)|0 = quantum_relative_entropy ρ σ
-/
def ψ (s : ℝ) := log tr ρ^{1 + s} * σ^{-s}
/-- "Legendre transformation of a convex function ψ(s)." -/
def φ (r : ℝ) := max {r * s - (ψ s) | 0 ≤ s ≤ 1}
theorem theorem1 (Aₙ : ℋ^⨂n →ₗ[ℂ] ℋ^⨂n) [test Aₙ] :
∀ r : ℝ,
1 - α σ Aₙ ≤ exp(-n*(φ ρ σ r)) + exp(n*r) • (β ρ Aₙ) :=
begin
intro r,
let s : ℝ := _,
/- "Define probability distributions pₙ and qₙ" -/
let pₙ := λ j, tr(ρ^⊗n * (Eₙ j)),
let qₙ := λ j, tr(σ^⊗n * (Eₙ j)),
have : Dₙ = {j | ∀ s [0 ≤ s ≤ 1], exp(-n*r*s) * (pₙ j / qₙ j)^s ≥ 1}, {
have : (μₙ j) * tr(Eₙ j) = (pₙ j) - exp(n*r) * (qₙ j), {
sorry
},
sorry,
},
calc tr(ρ^⊗n * (Xₙr μₙ Eₙ)) = ∑ j, if μₙ j ≥ 0 then tr(ρ^⊗n * Eₙ j) else 0 : by sorry
... = ∑ j, if μₙ j ≥ 0 then (pₙ j) else 0 : by sorry
... ≤ ∑ j, if μₙ j ≥ 0 then (pₙ j) • exp(-n*r*s) • (pₙ j / qₙ j)^s else 0 : by sorry
... ≤ exp(-n*r*s) * ∑ j, (pₙ j) * (pₙ j / qₙ j)^s : by sorry
... ≤ exp(-n*r*s) * tr((ρ^⊗n)^(1+s) * (σ^⊗n)^(-s)) : by sorry
... ≤ exp(-n * (r*s - (ψ s))) : by sorry
... ≤ exp(-n*(φ r)) : by sorry, -- "by taking the max"
calc 1 - α σ Aₙ = tr(ρ^⊗n * Aₙ) : by sorry
... ≤ tr(ρ^⊗n - exp(n*r) * σ^⊗n) • (Xₙr μₙ Eₙ) + exp(n*r) • tr(σ^⊗n * Aₙ) : by sorry -- lemma 1
... ≤ tr(ρ^⊗n * (Xₙr μₙ Eₙ)) + exp(n*r) • tr(σ^⊗n * Aₙ) : by sorry -- linarith
... ≤ exp(-n*(φ r)) + exp(n*r) • β ρ Aₙ : by sorry,
end
/-- Ogawa1999 -/
lemma liminf_geq_neg_rel_entropy :
∀ ε > 0,
liminf at_top (λn:ℕ, log(βmin ρ σ n ε)/n) ≥ - quantum_relative_entropy ρ σ :=
begin
intros ε Hε,
/- "Let Aₙ be some test s.t. prob_σₙ_when_ρₙ Aₙ ≤ ε." -/
let Aₙ := _,
let HAₙ := α σ Aₙ ≤ ε,
let n : ℕ := _,
have H1 : βmin ρ σ n ε ≥ exp(-n*r) * (1 - exp(-n*(φ ρ σ r)) - ε), {
calc βmin ρ σ n ε ≥ β ρ Aₙ : by sorry
... ≥ exp(-n*r) * (1 - exp(-n*(φ ρ σ r)) - α σ Aₙ) : by sorry -- theorem1
... ≥ exp(-n*r) * (1 - exp(-n*(φ ρ σ r)) - ε) : by sorry, -- "HAₙ"
},
let δ : ℝ := _,
let r := quantum_relative_entropy ρ σ + δ,
/- "Choose a large n. Such that φ r > 0. Then 1 - exp(-n*(φ r)) - ε is positive." -/
have : 1 - exp(-n*(φ r)) - ε > 0, {
have : φ r > 0, {
sorry,
},
sorry,
},
have H3 : log βmin ρ σ n ε / n ≥ -r + log(1 - exp(-n*(φ r)) - ε)/n, {
-- use H1, H2
sorry,
},
/- Take large n to get the statement of the lemma -/
sorry,
end
/-- Quantum Stein's lemma -/
lemma log_min_prob_tends_to_quantum_relative_entropy_for_sufficiently_many_systems :
∀ ε > 0,
lim λ n, log min_β_if_α_leq_ε n ε / n = - quantum_relative_entropy ρ σ :=
begin
-- follows from the two lemmas above
intros ε Hε,
apply lim_of_liminf_and_limsup_eq,
exact limsup_log_min_β_if_α_leq_ε_leq_neg_rel_entropy ε,
exact liminf_log_min_β_if_α_geq_ε_leq_neg_rel_entropy ε,
end
What does this mean in terms of click count in an experiment to distinguish quantum states?
∀ ε > 0 and ∀ δ > 0,
∃ large number of measurements n,
log min_β_if_α_leq_ε n ε / n = |- quantum_relative_entropy ρ σ + δ|
Some probability converges to a number that is a function of the quantum relative entropy. Such that when the quantum relative entropy increases, the probability of error decreases. a number we can compute: quantum relative entropy between two given states. an experiment we can perform: measure POVM at output of information source, then output if rho or sigma. qre is estimate of error.
This tells us we can Distinguish quantum states better if they are very different?
In Generalized quantum Stein lemma we allow states more general than tensor power states σ^⊗n.