## Stream: maths

### Topic: Non-positive-definite inner product spaces

#### Eric Wieser (Feb 01 2021 at 09:59):

Currently, docs#inner_product_space requires positive definite-ness.
nLab suggests that this is not a necessary condition for something to be an "inner product space", while wikipedia suggests that it is a necessary condition.

Without wanting to argue about whether the mathlib definition is correct, what would be a suitable name for the version whose inner product is not-necessarily-positive definite?

#### Kevin Buzzard (Feb 01 2021 at 10:00):

"space equipped with a symmetric bilinear form"?

#### Kevin Buzzard (Feb 01 2021 at 10:02):

I've never seen the nLab's convention used anywhere else BTW

#### Andrea Berlingieri (Feb 01 2021 at 10:33):

Maybe it's a silly question, and slightly off-topic w.r.t. your question, but isn't Wikipedia's definition "problematic" when the inner product goes to $\mathbb{C}$ , since it is not linearly ordered and thus the positive definiteness condition doesn't make sense in that case?

#### Kevin Buzzard (Feb 01 2021 at 10:33):

in the C case you assume sesquilinearity so (x,x) is always real-valued.

#### Andrea Berlingieri (Feb 01 2021 at 10:34):

Oh, I see. Thanks.

#### Eric Wieser (Feb 01 2021 at 10:51):

To motivate my question - this comes up when wanting to work in minkowski spacetime, for instance, where one unit basis vector squares to -1. It would be nice to still get norm and inner notation(and maybe dist), and have at least the bits of inner_product_space that show they are consistent with each other

#### Yury G. Kudryashov (Feb 01 2021 at 14:44):

You can't have norm in this case because norm is a real-valued function, and in Minkowski spacetime some squared norms are negative.

#### Eric Wieser (Feb 01 2021 at 16:02):

Oh, that's a good point - and I guess dist also has a square-root in it that makes it undesirable there. So I guess I don't have a reason to care about lemmas for norm and dist

#### Jean-Philippe Burelle (Feb 04 2021 at 14:57):

Many useful lemmas actually only involve the squared norm, and can be useful in indefinite signature. For instance, the "Pythagorean theorem" works as-is. Cauchy-Schwarz can also be adapted, but there are different cases depending on the sign of the "squared norm" of the vectors.

Last updated: May 10 2021 at 07:15 UTC