Hilbert spaces is closed under scalar multiplication

Stream: new members

[Martin Plávala]

Dear all, I am looking into lean and trying to understand whether it is usable to formalize my research. I installed lean locally, it seems to work in VScode and now I ma trying to prove a simple lemma that for any finite-dimensional complex Hilbert space \mathcal{H} and for any \psi \in \mathcal{H} we have 2 * \psi \in \mathcal{H}. The goal is of course not to set in stone this groundbreaking result, but to finally figure out how to actually use lean beyond those in-browser games where everything is somehow already done.

So far I figured out the following:

import Mathlib.Data.Complex.Basic
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.Normed.Group.Basic
import Mathlib.LinearAlgebra.FiniteDimensional.Defs
import Mathlib.LinearAlgebra.TensorProduct.Basic
import Mathlib.Tactic

-- Define a Hilbert space (finite-dimensional complex inner product space)
variable {ℋ : Type _} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ]

and the lemma I am trying to prove should be

lemma scalar_mult_closed (ψ : ℋ) : (2 • ψ ∈ ℋ) := sorry

But this returns an error. Could you please point me to why?

[Ruben Van de Velde]

Because you're using set notation for a type. You could write:

lemma scalar_mult_closed (ψ : ℋ) : (2 • ψ ∈ (Set.univ : Set ℋ)) := sorry

and the proof is Set.mem_univ (2 • ψ). Now this doesn't use the structure of your space at all, because in type theory, the fact that the result of scalar multiplication lands in the same type ("set") is built into the type of the scalar multiplication function

[Martin Plávala]

Ruben Van de Velde said:

Because you're using set notation for a type. You could write:

lemma scalar_mult_closed (ψ : ℋ) : (2 • ψ ∈ (Set.univ : Set ℋ)) := sorry

and the proof is Set.mem_univ (2 • ψ). Now this doesn't use the structure of your space at all, because in type theory, the fact that the result of scalar multiplication lands in the same type ("set") is built into the type of the scalar multiplication function

I'm sorry but could you explain that? Clearly I can have subsets of any Hilbert space which have scalar multiplication defined on them but are not closed under all possible multiples (e.g. take a cone closed only under positive multiples). Does that mean these do not exist in lean?

Also, should not the Hilbert space H be a set by definition?

[Ruben Van de Velde]

No, I think you do want your space H to be a type - you can then look at the Set that contains all the elements in your space (that's Set.univ), or at subsets

[Ruben Van de Velde]

The 2 • ψ you use is defined as ψ + ψ, where the addition comes from the NormedAddCommGroup H assumption, which defines addition as a function H → H → H

[Ruben Van de Velde]

That is, if you ever construct a specific Hilbert space, you'll have to define what addition means, and at that point prove that adding two elements of your space still lands inside the space

[Martin Plávala]

But then (ψ : ℋ) means that ψ is a Hilbert space itself?

[Ruben Van de Velde]

No, ψ is any element of H

[Ruben Van de Velde]

You could do something like this with subsets:

example (ψ : ℋ) (h : ψ ∈ ({0} : Set ℋ)) : (2 • ψ ∈ ({0} : Set ℋ)) := by
  simp_all

[Martin Plávala]

Thanks for the explanations. Could you please recommend some working level and not overtly theoretical introduction to lean then? It seems I am missing the points.

[Ruben Van de Velde]

In this case, 2 • ψ is an element of H by definition of scalar multiplication (and addition), but not of the subset {0}, so there's something (not much) to prove

[Ruben Van de Velde]

Maybe #mil is a good start

[Kevin Buzzard]

@Martin Plávala the question in your original post does not make any sense in Lean because multiplication by 2 on an additive abelian group A is defined to be a map from A to A so 2 • ψ is what you like to call an "element of A" automatically. Type theory is different to set theory. In set theory you can have a "thing" which is an element of many sets all at once. In type theory every term has exactly one type -- distinct types are disjoint. It is not possible to prove that 2 • ψ is a term of type ℋ -- every term has a type, and the type of 2 • ψ is ℋ because 2 • _ is a map from ℋ to ℋ so that's the end of it. You can do #check (2 • ψ) to make sure that this is the case:

import Mathlib

-- Let `ℋ` be  a finite-dimensional complex inner product space
variable {ℋ : Type _} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ]

-- Let `ψ` be an element of `ℋ`.
variable (ψ : ℋ)

-- Then 2ψ is also an element of `ℋ`.
#check 2 • ψ -- 2 • ψ : ℋ

Here is what I tell my maths undergrads about type theory. There is also this old blog post of mine.

[Martin Plávala]

Thanks for the reply! I am starting to understand what is going on here and it seems a lot like object oriented programming. In the end I discovered I can do

import Mathlib.Data.Complex.Basic
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.Normed.Group.Basic
import Mathlib.LinearAlgebra.FiniteDimensional.Defs
import Mathlib.LinearAlgebra.TensorProduct.Basic
import Mathlib.Tactic

-- Define a Hilbert space (finite-dimensional complex inner product space)
variable {ℋ : Type _} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ]

lemma scalar_mult_closed (ψ : ℋ) (α : ℂ) : (α • ψ ∈ (Set.univ : Set ℋ)) := by
  exact Set.mem_univ (α • ψ)

which actually works as intended.