Inner product space

Stream: general

[Joe]

I'd like to ask people for ideas on how to define an inner product/Hilbert space. I think it is good to keep things simple and define real and complex inner product spaces separately. But my guess is that people want to define them in a unified way. I'm not sure how to do that.

Furthermore, is there a definition of inner product spaces on more general fields besides real and complex ones?

[Joe]

I defined real inner product space at https://github.com/leanprover-community/mathlib/pull/1248.

[Joe]

class inner_product_space (α : Type*) extends add_comm_group α, vector_space ℝ α, has_inner α :=
    (comm      : ∀ x y, inner x y = inner y x)
    (nonneg    : ∀ x, 0 ≤ inner x x)
    (definite  : ∀ x, inner x x = 0 → x = 0)
    (add_left  : ∀ x y z, inner (x + y) z = inner x z + inner y z)
    (smul_left : ∀ x y r, inner (r • x) y = r * inner x y)

[Joe]

Here's @Andreas Swerdlow 's defintion of complex inner product space. https://github.com/leanprover-community/mathlib/pull/840.

[Joe]

class herm_inner_product_space (α : Type*) [add_comm_group α] [vector_space ℂ α] extends sesq_form ℂ α conj.ring_invo :=
    (to_sym_sesq_form : sym_sesq_form.is_sym to_sesq_form)
    (sesq_self_re_nonneg : ∀ (x : α), 0 ≤ (sesq x x).re)
    (sesq_self_eq_zero_iff : ∀ (x : α), sesq x x = 0 ↔ x = 0)

[Joe]

structure sesq_form (α : Type u) (β : Type v) [ring α] (I : ring_invo α) [add_comm_group β] [module α β] :=
    (sesq : β → β → α)
    (sesq_add_left : ∀ (x y z : β), sesq (x + y) z = sesq x z + sesq y z)
    (sesq_smul_left : ∀ (a : α) (x y : β), sesq (a • x) y = a * (sesq x y))
    (sesq_add_right : ∀ (x y z : β), sesq x (y + z) = sesq x y + sesq x z)
    (sesq_smul_right : ∀ (a : α) (x y : β), sesq x (a • y) = (I a) * (sesq x y))

[Joe]

structure ring_invo [ring R] :=
    (to_fun : R → R)
    [anti_hom : is_ring_anti_hom to_fun]
    (to_fun_to_fun : ∀ x, to_fun (to_fun x) = x)

[Joe]

Finally, @Scott Morrison thinks it is better to have a unified approach to real and complex inner product space. Here's his suggestion:

[Joe]

import analysis.normed_space.basic

class scalars (α : Type) extends normed_field α :=
(embed_ℝ : ℝ → α)
(conj : α → α) -- TODO axioms about conj

instance embed_ℝ_coe (α : Type) [scalars α] : has_coe ℝ α :=
{ coe := scalars.embed_ℝ α }

variables (α : Type) [scalars α]

example : α := (1 : ℝ)

notation a `†`:120 := scalars.conj a

set_option class.instance_max_depth 34
class sesquilinear_space (𝕶 : Type) [scalars 𝕶] (α : Type*) [add_comm_group α] [vector_space 𝕶 α] :=
(inner_product : α → α → 𝕶)
(conj_symm : ∀ (x y : α), inner_product x y = (inner_product y x)†)
(linearity : ∀ (x y z : α), ∀ (a : 𝕶), inner_product (a • x + y) z = a * inner_product x z + inner_product y z)

class inner_product_space (𝕶 : Type) [scalars 𝕶] (α : Type*) [add_comm_group α] [vector_space 𝕶 α]
  extends sesquilinear_space 𝕶 α, normed_space 𝕶 α :=
(norm_sq : ∀ (x : α), inner_product x x = (norm x)^2)

[Johan Commelin]

But sesquilinear forms are defined even more generally right? I don't think that scalars should ask for an embedding of the reals. I want sesquilinear forms over $\mathbb{Q}(i)$ :grinning_face_with_smiling_eyes:

[Johan Commelin]

I'm not saying that we should immediately formalise the most general thing possible. But it might be good to keep those generalisations in the back of our mind while formalising. If we do that, then refactoring/generalising the code might become easier in the future.

[Andrew Ashworth]

Too much abstraction nonsense makes it hard to get going. I vote for reals and complexes, since those are the only ones I've ever actually used :). Especially for experimental code like everyone here is writing, I wouldn't spend too much time overthinking things because odds are it'll need redoing anyway...

[Andrew Ashworth]

It would be pretty cool to one day use #eval and get the angle between two vectors using the inner product and arccos...

[Kevin Buzzard]

It seems to me that linear forms and sesquilinear forms are two different things. One could "unify" them both by giving a field K and a map c : K -> K and then consider forms (v,w) with (kv,w)=c(k)(v,w) but then if you choose to do linear forms this way you set c = identity and then have some useless identity map kicking around everywhere.

@Andrew Ashworth number theorists use sesquilinear forms over fields like the rationals all over the place in the Langlands programme.

[Andreas Swerdlow]

If we're going to do the real and complex cases separately, then they should at least have a similar style. Maybe a merger of mine and @Joe's files would work best. Specifically, still having real/complex inner product extend bilinear/sesquilinear form, but using Joe's more concise proof of Cauchy-Schwarz etc.

[Scott Morrison]

Has anyone looked at the good textbooks for Hilbert spaces? Amongst the more "good references, but you wouldn't want to learn from them" choices: Bourbaki "Topological vector spaces" chapter 5 does the real and complex cases together, as does Pedersen "Analysis Now"

[Jeremy Avigad]

I am also not convinced that the extra abstraction is helpful rather than a hindrance now. It is similarly unfortunate that we have gcd defined on nat and int independently, but a common generalization will probably be more trouble than it is worth. My suggestion would be to unify the inner products when we have good reason to. Such a reason will then give us more information as to what the unification should be.

[Scott Morrison]

Okay, I'm sold. Looking at both Bourbaki and Pedersen, it seems that they really use a typeclass is_R_or_C on their field! That is, mostly they pretend they have an arbitrary field with conjugation, but occasionally they break into those two cases. It seems the majority of the times they need to case bash are to use polarisation identities (writing inner products as a linear combination of norms), but that the arguments nearly always converging quickly again after using polarisation.

[Scott Morrison]

Perhaps a good solution would be for whoever develops real and/or complex inner product spaces to try to follow a book that attempts to handle both cases in a fairly uniform fashion. That way the two parallel developments shouldn't stray too far from each other.