Bug report on Generalized quantum Stein lemma

• Lean does not accept proof of Generalised quantum Stein’s lemma in Plenio2009.

  • A sorry in Lemma III.9.

    • Lemma III.9 depends on III6, C6 and III10

  • “In the proof of lemma III9 of Plenio2009, it is argued that

variables
(m r : ℕ)
[τ > 0]
[n ≥ m + r]

/-- ?? -/
def g((μ 1 n), (μ 2 n), ...) :=
1/n * (∑ j, (t j n)(log(μ j n))² - (∑ j, (t j n)(log(μ j n)))²)

notation `the_g` := g((μ 1 n), (μ 2 n), ...)

def tₙ := τ/(1+τ) λmin(σ)^{n-m-r}

/--
when maximized over all distributions
that satisfy ∀ j ∈ 𝒳^{n-m-r}, (μ j n) ≥ tₙ,
where 𝒳^{n-m-r} is a finite set,
achieves its maximum when all (μ j n) except one are equal to t."
-/
lemma max_of_the_g : max{the_g | ∀ j ∈ 𝒳^{n-m-r}, (μ j n) ≥ tₙ} = the_g(...) :=
begin
  sorry,
end

/--
"The authors then use this to conclude that
∃ k, ∀ n > k, g((μ 1 n), (μ 2 n), ...) ≤ 1
if the sequence of prob. dist. {(μ j n)}ₙ have
their minimum probability ≥ tₙ."
-/
lemma broken :
∀ n, min (μ j n) ≥ tₙ
→
∃ k, ∀ n > k,
g((μ 1 n), (μ 2 n), ...) ≤ 1 :=
begin
  sorry,
end

• “The lemma statement is false. Counter-example.”

  • “Error in eq. 147 in Plenio2009: We must have ∑ j ∈ 𝒳^{n-m-r}, (μ j n) = 1.”

• Notation:

  • Dmax(ρ

    σ) := log min{λ ≥ 1

    ρ ≤ λ * σ}

    • “max relative entropy”
  • ANE := asymptotically non-entangling operations

---

• Dependent libraries that are potentially affected:

  • General quantum resources [Brandão & Gour, Phys. Rev. Lett. 115, 070503 (2015)]

    • under asymptotically resource non-generating operations.

  • Gour2021

    • This is where the mistake was identified: A sorry in lemma Lemma16;

References

• Plenio2022;