Zulip Chat Archive
Stream: general
Topic: Inner product spaces
Alexander Bentkamp (Mar 15 2019 at 20:15):
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/xenaUROP2018/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 (Mar 15 2019 at 20:19):
There is the whole theory of quadratic forms, which works over any field (though characteristic 2 can be hairy).
Johan Commelin (Mar 15 2019 at 20:20):
Then you can specialise to nondegenerate forms, symmetric forms, alternating forms, hermitian forms, etc...
Kevin Buzzard (Mar 15 2019 at 20:30):
In number theory we define unitary groups in the setting where K is a field (say) and L/K is a finite etale Kalgebra of degree 2, which is a fancy way of saying either L=K+K or L is a separable quadratic extension of K. The nontrivial Kautomorphism of L is denoted c, say (c for complex conjugation if K=real and L=complex) and then one can consider a nondegenerate hermitian sesquilinear form on an Lvector space. For it to be positive definite you need some notion of positive though, so then K should embed into the reals.
Alexander Bentkamp (Mar 15 2019 at 20:54):
Ok, thanks. I'll see what I can do.
Andreas Swerdlow (Mar 16 2019 at 02:41):
I was thinking of submitting to mathlib fairly soon. A more up to date version is available here: https://github.com/leanproverfork/mathlibbackup/blob/inner_product_spaces/linear_algebra/herm_inner_product_space.lean
Alexander Bentkamp (Mar 16 2019 at 17:34):
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 (Jun 17 2021 at 12:02):
As suggested by @Heather Macbeth, I'm looking at proving Bessel's inequality. I have a couple of basic questions.

If I explicitly include the instance
[normed_group E]
below, Lean complains that it couldn't synthesize a type class instance foradd_comm_monoid E
. Why is that? I thoughtinner_product_space
extendsnormed_group
. What do I have to do to fix this? 
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 (Jun 17 2021 at 12:08):
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 (Jun 17 2021 at 12:28):
Thanks. I suppose sesquilinear for Bessel's inequality.
As far as I can tell, the code at analysis.normed_space.inner_product#propertiesofinnerproductspaces 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 (Jun 17 2021 at 12:55):
Aah yes, this seems to be the trick used on line 151 of the file. Nice!
Kevin Buzzard (Jun 17 2021 at 12:55):
I couldn't understand your other question. Can you show me the error?
Rémy Degenne (Jun 17 2021 at 13:01):
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 (Jun 17 2021 at 13:01):
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 (Jun 17 2021 at 13:02):
I would advise against redefining the notation. Simply open the namespace.
Gihan Marasingha (Jun 17 2021 at 13:03):
Thanks @Rémy Degenne and @Yaël Dillies. That's working much better.
Gihan Marasingha (Jun 17 2021 at 13:20):
@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
!
Last updated: Aug 03 2023 at 10:10 UTC