Zulip Chat Archive

Stream: general

Topic: Inner product space


Joe (Jul 26 2019 at 04:01):

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 (Jul 26 2019 at 04:02):

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

Joe (Jul 26 2019 at 04:02):

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 (Jul 26 2019 at 04:03):

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

Joe (Jul 26 2019 at 04:05):

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 (Jul 26 2019 at 04:06):

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 (Jul 26 2019 at 04:07):

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 (Jul 26 2019 at 04:08):

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

Joe (Jul 26 2019 at 04:09):

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 (Jul 26 2019 at 06:14):

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 Q(i)\mathbb{Q}(i) :grinning_face_with_smiling_eyes:

Johan Commelin (Jul 26 2019 at 06:15):

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 (Jul 26 2019 at 08:37):

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 (Jul 26 2019 at 08:42):

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 (Jul 26 2019 at 08:47):

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 (Jul 26 2019 at 09:32):

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 (Jul 26 2019 at 10:44):

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 (Jul 26 2019 at 14:47):

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 (Jul 27 2019 at 00:09):

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 (Jul 27 2019 at 00:10):

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.


Last updated: Dec 20 2023 at 11:08 UTC