Inner product spaces

Stream: general

[Alexander Bentkamp]

Hello,
Is there anyone else currently interested in inner product spaces? I'd like to start working on this.

I found this formalization:
https://github.com/ImperialCollegeLondon/xena-UROP-2018/blob/master/src/inner_product_spaces/basic.lean.
@Andreas Swerdlow Are there still plans to bring this into mathlib?

I am also aware of the Lean2 formalization: https://github.com/leanprover/lean2/blob/master/library/theories/analysis/inner_product.lean

The ImperialCollege formalization is over complex numbers and the Lean2 formalization is over the reals. I am interested in the reals, but I will try to find a generalization that subsumes both. Are there any concepts like this already?

[Johan Commelin]

There is the whole theory of quadratic forms, which works over any field (though characteristic 2 can be hairy).

[Johan Commelin]

Then you can specialise to nondegenerate forms, symmetric forms, alternating forms, hermitian forms, etc...

[Kevin Buzzard]

In number theory we define unitary groups in the setting where K is a field (say) and L/K is a finite etale K-algebra of degree 2, which is a fancy way of saying either L=K+K or L is a separable quadratic extension of K. The non-trivial K-automorphism of L is denoted c, say (c for complex conjugation if K=real and L=complex) and then one can consider a non-degenerate hermitian sesquilinear form on an L-vector space. For it to be positive definite you need some notion of positive though, so then K should embed into the reals.

[Alexander Bentkamp]

Ok, thanks. I'll see what I can do.

[Andreas Swerdlow]

I was thinking of submitting to mathlib fairly soon. A more up to date version is available here: https://github.com/leanprover-fork/mathlib-backup/blob/inner_product_spaces/linear_algebra/herm_inner_product_space.lean

[Alexander Bentkamp]

I have transferred the Lean2 formalization to Lean3 now. It's for real vector spaces only. Let's see if we can merge after you submit to mathlib.

[Gihan Marasingha]

As suggested by @Heather Macbeth, I'm looking at proving Bessel's inequality. I have a couple of basic questions.

1. If I explicitly include the instance [normed_group E] below, Lean complains that it couldn't synthesize a type class instance for add_comm_monoid E. Why is that? I thought inner_product_space extends normed_group. What do I have to do to fix this?

2. Lean doesn't like my use of the⟪·, ·⟫ notation here. It seems to work fine if I put the example directly in the analysis.normed_space.inner_product file. How do I use the notation outside that file?

import analysis.normed_space.inner_product data.complex.is_R_or_C

open_locale big_operators

variables {𝕜 E ι: Type*} [is_R_or_C 𝕜]  [inner_product_space 𝕜 E] [complete_space E]

example {ι : Type*} (s : finset ι) [normed_group E] (f : ι → E) : E :=  ∑ i in s, f i

example {ι : Type*} (s : finset ι) [normed_group E] (f : ι → E) (x : E) : E :=
x -  ∑ i in s, ⟪x, f i⟫ • (f i) -- doesn't work.

[Kevin Buzzard]

Notation:

localized "notation `⟪`x`, `y`⟫` := @inner ℝ _ _ x y" in real_inner_product_space
localized "notation `⟪`x`, `y`⟫` := @inner ℂ _ _ x y" in complex_inner_product_space

means "if you want to use this notation, write open_locale real_inner_product_space resp complex_inner_product_space -- but do you want to be linear or sesquilinear?

[Gihan Marasingha]

Thanks. I suppose sesquilinear for Bessel's inequality.

As far as I can tell, the code at analysis.normed_space.inner_product#properties-of-inner-product-spaces uses the ⟪·, ·⟫ notion for both real and complex inner product spaces. I've found that stealing the line:

local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y

just above my example makes Lean stop complaining. Hopefully that's the right thing to do here!

[Kevin Buzzard]

Aah yes, this seems to be the trick used on line 151 of the file. Nice!

[Kevin Buzzard]

I couldn't understand your other question. Can you show me the error?

[Rémy Degenne]

Nothing in the examples mentions 𝕜, hence that type and all instances that depend on it are not in the context. If you look at the context in the first example, there is no inner_product_space 𝕜 E

[Rémy Degenne]

This works:

import analysis.normed_space.inner_product data.complex.is_R_or_C

open_locale big_operators

variables {𝕜 E ι: Type*} [is_R_or_C 𝕜]  [inner_product_space 𝕜 E] [complete_space E]

include 𝕜
example {ι : Type*} (s : finset ι) (f : ι → E) : E :=  ∑ i in s, f i
omit 𝕜

[Yaël Dillies]

I would advise against redefining the notation. Simply open the namespace.

[Gihan Marasingha]

Thanks @Rémy Degenne and @Yaël Dillies. That's working much better.

[Gihan Marasingha]

@Kevin Buzzard as per @Rémy Degenne's comment, my error was that I hadn't included 𝕜 in the context so I wasn't really dealing with an instance of inner_product_space 𝕜 E!