Generalized Quantum Stein's Lemma

Stream: Quantum information

[Alex Meiburg]

Thread for the work that mostly @Rodolfo R. Soldati , @Léo Lessa and I have been working on. I'm in the middle of some cleanup at the moment but I want to write a better update soon

[Alex Meiburg]

I bumped the mathlib version. Also moved a bunch of floating lemmas to the right places. :) And we can use the lemmas from #27115 that were upstreamed, yay

[Jenkin]

Hi everyone, I am trying to formalize the Schmidt decomposition Theorem 3.8.1 in Mark Wilde's book, but I am not sure how to say that a set of (Ket d) is Orthonormal. I tried Orthonormal ℂ (fun i ↦ (φ i).vec) but it returns an error. Any ideas? Thanks!

The theorem statement I have so far is

theorem SchmidtDecomposition (ψ : Ket (d₁ × d₂)) :
∃ (a : d → ℝ) (φ : d → Ket d₁) (η : d → Ket d₂),
ψ = ∑ i, (a i) • (Ket.prod (φ i) (η i)).vec :=
sorry

[Alex Meiburg]

The issue is that Orthonormal requires a notion of inner product, but a "raw" function like (φ i).vec doesn't have an inner product associated to it. (What if i was infinite? Then a naive sum might not converge.)

The type EuclideanSpace ℂ d is equal, under the hood, to a raw function, but it instructs Lean to use the PiLp.innerProductSpace instance to give it an inner product structure.

[Alex Meiburg]

So if you try something like Orthonormal ℂ (fun i ↦ (φ i).vec), you'll get the error message

failed to synthesize
  InnerProductSpace ℂ (d₁ → ℂ)

or similar, which can help point you in this direction.

So how do you fix this?

[Alex Meiburg]

Well, actually in Braket.lean there is a note saying

--TODO: change to `vec : EuclideanSpace ℂ d`

so it's already been on my mind. :) And I think @Rodolfo R. Soldati has played a bit with doing this change, I'm not sure if the code is anywhere online though

[Alex Meiburg]

But for the moment, you can get around this by just casting. The easiest way to write this is to use docs#WithLp.toLp to turn the raw function into a vector in EuclideanSpace. So this should work:

have := Orthonormal ℂ (fun i ↦ WithLp.toLp 2 (φ i).vec)

[Alex Meiburg]

Note that it will technically give it the type WithLp 2 (d → ℂ), not EuclideanSpace ℂ d, but these are _really_ the same thing, and any place you use one the other should work too.

[Rodolfo Soldati]

I will try to give maybe a pull request before the end of the day so we can discuss around it

[Rodolfo Soldati]

I should reach the SVD soon, but I'm using Watrous's book

[Jireh Loreaux]

FYI, Niels Voss is already working on SVD and the Schmidt decomposition. See #Is there code for X? > Singular Value Decomposition @ 💬