Complex inner product

Stream: maths

[Keefer Rowan]

I was thinking as my first contribution to mathlib making complex_inner_product.lean which basically duplicates real_inner_product.lean but for complex inner product spaces. Is this a good idea? If so what should I name the inner product operation? Right now there is the class has_inner with operation inner : \alpha \to \alpha \to \R. Should I make a class has_cinner with operation cinner : \alpha \to \alpha \to \C or generalize has_inner to have inner : \alpha \to \alpha \to \beta?

[Johan Commelin]

I fear that the trouble with \a → \a → \b is that it can't infer \b from the arguments of the inner product. So you would have to mark \b as an out_param, and I don't understand those.

[Reid Barton]

Last time I looked, this already existed, but in a completely different part of mathlib, I think.

[Keefer Rowan]

@Reid Barton A complex_inner_product.lean file? I couldn't find anything in Linear Algebra. There was some other branch that was being developed but it seems to have been called off.

[Johan Commelin]

@Reid Barton git grep inner doesn't show anything interesting outside real_inner_product.lean

[Keefer Rowan]

@Johan Commelin So has_cinner then?

[Johan Commelin]

Well....

[Reid Barton]

Am I confusing this with something else?

[Johan Commelin]

What if someone wants to do inner products over $\mathbb{Q}(\sqrt{-5})$?

[Johan Commelin]

We would end up with 10.000 classes. So I think we should search for a good generalisation.

[Reid Barton]

Maybe it was already refactored: linear_algebra.sesquilinear_form

[Johan Commelin]

But it's not immediate (to me) what it should be.

[Johan Commelin]

aha, so we already have a general theory...

[Johan Commelin]

@Keefer Rowan Maybe this is not the best first project... how about doing so stuff over at the real side?

[Johan Commelin]

I would love to see Sylvester's law of inertia in mathlib

[Johan Commelin]

Maybe something with diagonalizing matrices

[Keefer Rowan]

So should complex inner product not be defined as a class, just as write theorems about sesquilinear form with a specific anti-iso?

[Keefer Rowan]

@Johan Commelin I’m more of an analyst than an algebraist. I just wanted basic theory to get into Hilbert space stuff

[Johan Commelin]

Ok, I don't know anything about Hilbert spaces

[Johan Commelin]

But we certainly want those

[Keefer Rowan]

I just basic stuff about complex inner product spaces. Existence of orthogonal projection. That sort of thing. A Hilbert space is just a complex inner product space that is complete w/r/t the norm metric

[Johan Commelin]

And I guess we want some form of notation for inner products... but the obvious angle brackets are reserved by Lean.

[Johan Commelin]

@Keefer Rowan If the notation mentions the ground field, then we can easily solve the problem.

[Keefer Rowan]

So first it makes sense to prove basic facts to prove stuff about complex inner product spaces. And yeah notation would be nice

[Keefer Rowan]

any ideas?

[Johan Commelin]

You could write something like $\langle a, b \rangle_K$, where $K = \mathbb{R}$ or $\mathbb{C}$.

[Johan Commelin]

Does that look acceptable?

[Johan Commelin]

In Lean it would become something more like ⟨a,b⟩[K]

[Johan Commelin]

Because we can't do proper subscripts

[Johan Commelin]

The other option is to try the out_param thing

[Keefer Rowan]

I’m a bit confused as to why the output can’t be inferred. If there is no only one inner product instance over alpha can’t it figure out the output type?

[Sebastien Gouezel]

Don't play the outparam game, because one day you may want to look at a complex vector space as a real vector space.

[Johan Commelin]

@Sebastien Gouezel But that would be restrict_scalars real complex V, right?

[Keefer Rowan]

Correct me if I’m wrong, but aren’t the only two proper inner product the real and complex inner products. Then one can worry about sesquilinear forms in a general algebraic setting, but it seems like it’d be fine to have a complex inner product class and a real inner product class

[Johan Commelin]

Maybe they cover all the cases where you want notation...

[Johan Commelin]

I'm not sure though

[Sebastien Gouezel]

It wouldn't have to be restrict_scalars real complex V. This type synonym is helpful when you have many fields and you want to do algebra. The situation with complex and real is sufficiently canonical that we have instances declaring that a complex space is also a real space. For instance, we have

instance normed_space.restrict_scalars_real (E : Type*) [normed_group E] [normed_space ℂ E] :
  normed_space ℝ E

in analysis/complex/basic. It makes it possible to apply for free theorems on the topology of real vector spaces to complex vector spaces.

[Johan Commelin]

My alter ego pretty often considers examples of inner products over number fields.

[Johan Commelin]

And my alter ego does use bracket notation for them

[Johan Commelin]

@Sebastien Gouezel So, what do you suggest? Use notation that mentions the base field? Or no notation at all? Or separate classes for R and C?

[Keefer Rowan]

I mean for now we can just do no notation explicit variable base field

[Sebastien Gouezel]

I would say: keep the current notation for the real scalar product, and put an index c to denote a complex hermitian product. If we could have an index ℂ this would be awesome, but I am not sure unicode has considered this.

[Johan Commelin]

So separate classes, and ignore fields that aren't real or complex.

[Keefer Rowan]

What should the class be called? has_cinner or has_innerc?

[Sebastien Gouezel]

Yes, I would go for separate classes for now. I don't know if there is a satisfactory math unification.

[Johan Commelin]

Doesn't matter. I think I would go for innerc

[Patrick Massot]

Maybe I've read that thread too quickly, but I don't understand this complex inner product non-sense. I don't think anyone use this. The definition of complex Hilbert spaces certainly don't, it's all about sesquilinear forms

[Patrick Massot]

If the issue is simply that you call complex inner product what is usually called hermitian product then the answer is we already have them

[Sebastien Gouezel]

I can't find hermitian anywhere in mathlib.

[Keefer Rowan]

@Patrick Massot I don't see why you call this "nonsense". A very standard definition of a complex Hilbert space is a complex inner product space that is complete w/r/t to the norm metric. Do you have a better definition?

Maybe you are right about the terminological confusion; I think "complex inner product" is standard, e.g. in Folland, Real Analysis. Are you thinking of complex inner product as symmetric as opposed to hermitian?

[Keefer Rowan]

I think there was a branch that developed Hermitian inner products but it was closed/given up on for some reason and never merged to master.

[Scott Morrison]

There was also a thread about this exact question from July last year.

[Scott Morrison]

My suggestion from then had been:

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.

[Reid Barton]

Bourbaki doesn't consider quaternionic Hilbert spaces??

[Patrick Massot]

Maybe this is a French/English translation issue

[Patrick Massot]

@Keefer Rowan what's wrong with https://leanprover-community.github.io/mathlib_docs/linear_algebra/sesquilinear_form.html?

[Reid Barton]

(I don't know if these even make sense)

[Keefer Rowan]

@Patrick Massot Sesquilinear forms aren't positive definite, correct?

[Patrick Massot]

positive definite ones are a special case

[Patrick Massot]

In general they aren't

[Scott Morrison]

This had been my suggestion from last year (since then someone has done sesquilinear forms):

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)

[Keefer Rowan]

Of course, a complex inner product is a type of sesquilinear form, but they have an additional axiom and some nice properties that don't hold in general. Don't they deserve to be developed in their own right? Perhaps for algebraists or whomever they aren't very special, but in functional analysis, they are usually developed in their own right.

[Scott Morrison]

I think Patrick is just saying they should be built on top of sesquilinear forms, rather than from scratch.

[Scott Morrison]

There's no need to prove all the facts which are true for merely sesquilinear forms a second time for inner products.

[Johan Commelin]

@Scott Morrison But will type class search work with your setup?

[Johan Commelin]

If I have x y : V, and I write inner x y (or use whatever notation), then how will Lean figure out the scalars?

[Keefer Rowan]

Shouldn't we define innerc_product_space as usual and then prove it is an instance of a sesquilinear form?

[Scott Morrison]

Oh, I see. I think you should have to specify the field, and you can use local notations to hide it when you want to specialise to real and complex

[Keefer Rowan]

I think you pretty much always have to do the proof for real and complex separately, even though they are often similar.

[Scott Morrison]

@Keefer Rowan, what do you mean by "as usual"? If it's going to be a structure with the same fields as sesq_form (and some extras) then it's seems pretty reasonable to begin by extending sesq_form.

[Scott Morrison]

Those books I mentioned above, Bourbaki's Topological Vector Spaces and Pedersen's Analysis Now, both do what looks like a nice job of keeping the real and complex cases parallel.

[Scott Morrison]

They need to case split whenever they use polarisation, but manage to get the statements parallel for a long time.

[Scott Morrison]

My guess is that either would be a pretty nice to follow while formalising. (Even though Pedersen is not the greatest book to learn from.)

[Johan Commelin]

Ideally, most of this works for fields "with a conjugation (which might be trivial)"

[Keefer Rowan]

I'm really not sure how it would look to develop this in full proper generality. The standard informal development would have you working over $\mathbb{F} = \mathbb{C}$ or $\mathbb{R}$ and then you write proofs for $\mathbb{C}$ that also work for $\mathbb{R}$ (since there is an informal "coercion" $\mathbb{R} \to \mathbb{C}$). But I don't see how we define inner products this way in Lean and even if we did I don't see how to do "both proofs at once". It seems much more staightforward to just define two classes and "prove everything twice", even though mostly the same proofs will work. Now if we are trying to do Johan's much more general situation, then it makes sense to try to do everything in much more generality. I'm not sure how the positive-definiteness condition works in this general case though.

[Scott Morrison]

I'd be interested in trying to express positivity as ∀ (x : α), sesq x x = (norm x)^2. That is, you separately assume sesq_form and normed_space, and assert positivity by saying they are related in this way. It covers the real and complex cases, at least, and then otherwise I don't know if it's useless or useful, but who cares.

[Johan Commelin]

@Keefer Rowan I haven't thought through all the details, but there is the (useful to me) notion of "totally definite".

[Scott Morrison]

From my dim memory (I haven't looked since last July), this is how Bourbaki does it?

[Johan Commelin]

Do you need that R is totally ordered? Or is it enough to have a notion of positive elements?

[Scott Morrison]

(That might be totally wrong...)

[Johan Commelin]

@Scott Morrison your suggestion requires a normed field.

[Scott Morrison]

Yes

[Johan Commelin]

I would like to experiment with how far you can get with a (non-totally) ordered field and a quadratic extension.

[Scott Morrison]

There are non-normed fields?! :-)

[Johan Commelin]

Scott Morrison said:

There are non-normed fields?! :-)

Only on Wednesdays

[Johan Commelin]

@Scott Morrison @Keefer Rowan This is probably both too complicated and not general enough...

import logic.function.basic
import algebra.ordered_ring
import algebra.field
import ring_theory.algebra
import ring_theory.maps
import linear_algebra.sesquilinear_form
import analysis.complex.basic

section preps

set_option old_structure_cmd true

class ordered_field (F : Type*) extends ordered_ring F, field F

class has_conj (C : Type*) [semiring C] extends C →+* C :=
(involutive : function.involutive to_fun)

def conj {C : Type*} [semiring C] [I : has_conj C] : C →+* C := has_conj.to_ring_hom C

lemma conj_involutive (C : Type*) [semiring C] [I : has_conj C] :
  function.involutive (conj : C → C) := I.involutive

class real_complex_pair (R : Type*) (C : Type*) [ordered_field R] [field C]
  [has_conj C] [algebra R C] :=
(fix : ∀ z : C, conj z = z ↔ ∃ r : R, z = algebra_map R C r)

end preps

variables (R : Type*) (C : Type*) [ordered_field R] [field C]
  [has_conj C] [algebra R C] [real_complex_pair R C]

def conj_hom_anti_equiv : ring_anti_equiv C C :=
{ to_fun := conj,
  inv_fun := conj,
  left_inv := (conj_involutive C).left_inverse,
  right_inv := (conj_involutive C).right_inverse,
  anti_hom :=
  { map_one := conj.map_one,
    map_mul := λ x y, by { rw mul_comm, apply conj.map_mul, },
    map_add := conj.map_add }}

class inner_product_space (V : Type*) [add_comm_group V] [module C V]
  extends sesq_form C V (conj_hom_anti_equiv C) :=
(symm : ∀ x y, sesq x y = conj (sesq y x))
(pos  : ∀ x, ∃ r, 0 < r ∧ sesq x x = algebra_map R C r)

section examples
open complex

noncomputable instance complex.has_conj : has_conj ℂ :=
{ to_fun := conj,
  map_one' := conj_one,
  map_mul' := conj_mul,
  map_zero' := conj_zero,
  map_add' := conj_add,
  involutive := conj_involutive }

instance linear_ordered_field.ordered_field (R : Type*) [I : linear_ordered_field R] :
  ordered_field R := {..I}

noncomputable instance : real_complex_pair ℝ ℂ :=
{ fix := λ z, eq_conj_iff_real }

end examples

[Johan Commelin]

One big downside is that we still can't have nice notation.

[Keefer Rowan]

All this discussion has me wondering how much we will get out of working in this generality. Really I’m just interested in getting to Hilbert space and functional analysis and there’s not that much theory of general inner products that I’m familiar with so I can formalize. Would it be wrong to just do the complex inner product? How necessary is it to develop the theory in complete generality before doing the case that has extremely wide applicability?

[Mario Carneiro]

Actually even having a typeclass is_R_or_C would be a bit challenging

[Mario Carneiro]

it's probably easier to define is_R_or_C to mean "having all the common identities we want" like polarization

[Keefer Rowan]

Why not just have a real inner product type class and a complex one?

[Mario Carneiro]

presumably the reason the books talk about is_R_or_C is because there are a lot of duplicated lemmas

[Mario Carneiro]

we can also have a real and complex inner product type class if there is more structure there worth noting, but having one way to prove facts in both contexts seems good to me

[Keefer Rowan]

Yes, but it’s not clear that it’d make anything simpler doing it that way. Eg in the real case you won’t have trivial conjugations floating around. And I’m pretty sure to do any proof you would need to split by cases unless you compiled an absurdly long list of theorems that hold for R and C and show they hold for our is_R_or_C class.

[Scott Morrison]

I'm completely uncertain about the best approach here. It's a maintenance and pedagogical hassle later down the track if we have closely duplicated developments written at different times by different people. On the other hand:

<provocation>At the end of the day all that matters is the complex case. :-) </provocation>.

[Scott Morrison]

@Keefer Rowan, the contrary evidence is that there are textbooks that do this.

[Mario Carneiro]

Eg in the real case you won’t have trivial conjugations floating around

No, you will have exactly one trivial conjugation floating around

[Keefer Rowan]

Textbooks are informal. They can write proofs for complex case and let the reader do the necessary mental rewrites, type coercion, and whatnot.

[Mario Carneiro]

This "R or C" phenomenon is very widespread, and I have had to deal with it before in metamath. I stuck to my guns and just did "trivial generalization", using something like a division ring for as long as possible. It helped in that case that Norman Megill's personal research area was in orthonormal algebras and hilbert spaces over general division rings

[Mario Carneiro]

something to do with quantum logic

[Mario Carneiro]

We also used the concept of a *-ring, which is a ring with an order two automorphism (aka conjugation)

[Mario Carneiro]

How about: a field with a conjugation such that the fixpoints of the conjugation form a complete ordered field

[Mario Carneiro]

you don't even really need the order, since you can define it as "x is nonnegative if it is the square of a formally real element"

[Keefer Rowan]

What is the point of an arbitrary complete ordered field if that is just $\mathbb{R}$ upto iso?

[Keefer Rowan]

Also what about the idea of being able to recover most of the theorems for the real case from the complex case by using complexification which gives us a linear isometry (not surjective), so e.g. for Cauchy Schwarz, we get $|\langle x ,y \rangle | = |\langle U x, U y \rangle | \leq \| U x \| \| U y\| = \|x\| \|y\|$ where $U$ is the isometry? Perhaps many of the theorems can be recovered this way.

[Mario Carneiro]

Keefer Rowan said:

What is the point of an arbitrary complete ordered field if that is just $\mathbb{R}$ upto iso?

That is the point. This is just is_R_or_C, but stated in a way that doesn't involve type equality or messy isomorphisms

[Mario Carneiro]

also, we still have not proven that an arbitrary complete ordered field is just $\mathbb{R}$ up to iso and I have a vested interest in seeing that theorem proved, so writing things this way might encourage it

[Mario Carneiro]

Besides, there are other things that satisfy is_R_or_C that might not be real or complex, for example {x : complex // Re x = 0} or real^1

[Mario Carneiro]

Keefer Rowan said:

Also what about the idea of being able to recover most of the theorems for the real case from the complex case by using complexification which gives us a linear isometry (not surjective), so e.g. for Cauchy Schwarz, we get $|\langle x ,y \rangle | = |\langle U x, U y \rangle | \leq \| U x \| \| U y\| = \|x\| \|y\|$ where $U$ is the isometry? Perhaps many of the theorems can be recovered this way.

Perhaps, but the theorems I am thinking about are simple calculational things that can be stated but possibly not proved in a generic way. We want these to be easy to apply without constructing some embedding to complex all the time

[Johan Commelin]

Mario Carneiro said:

How about: a field with a conjugation such that the fixpoints of the conjugation form a complete ordered field

@Mario Carneiro did you look at my code above? I drop the completeness, because I use hermitian forms over number fields

[Mario Carneiro]

The nice thing about such a characterization is that there are obvious ways to weaken it when you don't need some properties like completeness. I would guess that for most algebraic properties of hilbert spaces you don't need completeness, but there are certainly theorems that need the vector space to be topologically complete, and it's not clear to me how often the scalar field also needs to be complete.

[Mario Carneiro]

In metamath we have a "pre-Hilbert space" which has all the structure of a Hilbert space but not the completeness requirements

[Mario Carneiro]

I forget if this is the same thing as an "inner product space"

[Mario Carneiro]

Ah yes, a "generalized pre-Hilbert space", a.k.a inner product space is a left module over a star-division-ring with an inner product that satisfies the usual rules

[Mario Carneiro]

Metamath has the polarization identity, but only for hilbert spaces over C, and the statement of the theorem explicitly uses i so it's not clear what the generalization is supposed to be

[Scott Morrison]

The real polarization identity is <f,g> = (||f+g||^2 - ||f-g||^2)/4. But the formula itself often doesn't matter: you just need the observation that the inner product is determined by the norm. Maybe there are some intermediate situations where knowing that the inner product is some linear combination of norm-squareds of linear functions of the inputs is good enough too?

[Mario Carneiro]

Oh interesting. this version looks closer to that but there are some additional terms:

$\langle f,g\rangle = \frac14 [(\|f+g\|^2 - \|f-g\|^2) + i(\|f+ig\|^2-\|f-ig\|^2)]$

[Mario Carneiro]

perhaps there is some reason the latter two terms cancel on some additional assumption about the inner product

[Yury G. Kudryashov]

The real inner product is the real part of the complex inner product (if you go from complex to real).

[Mario Carneiro]

/me wonders which meaning of "real" Scott meant

[Yury G. Kudryashov]

I guess he meant real inner product space. You can complexify it (new vectors are $f+ig$), then apply the complex result, then use the fact that the original inner product was real.

[Johan Commelin]

One thing that I took away from this thread is that the least we can do is to add a has_star class, which covers complex conjugation, but also the star operator on matrices.

[Johan Commelin]

And then we can bicker about what the weakest assumptions on a is_R_or_C class should be.

[Keefer Rowan]

I'm starting to think this project is a bit beyond me, as an analysis person, I'm not even really familiar with what ought to be formalized in this generality.

[Kevin Buzzard]

It is true that in the study of unitary groups, number theorists definitely need sesquilinear forms defined in number field situations. But this shouldn't be stopping an analyst from formalising Hilbert spaces. What is going on here? What is missing?

[Mario Carneiro]

My suggestion for a first pass is to do "trivial generalization" from what you know about complex inner product spaces. Use a general field or division ring, but make it C in your head and just ignore the fact that it is more general than that. Whenever a theorem fails to hold, add an assumption to make it hold

[Scott Morrison]

Sorry, @Keefer Rowan, you also shouldn't take our bikeshedding over the generality too seriously.

[Kevin Buzzard]

Right, this is what I'm saying. There are some issues here but I don't understand why it should affect Keefer

[Scott Morrison]

In my experience an excellent way to get the generality right is to first get it wrong, thereby inspiring someone to take a second pass.

[Kevin Buzzard]

i.e. just ignore all this stuff and write the code anyway

[Frédéric Dupuis]

Hi,

It turns out that I got started on this exact project to start learning Lean and I just found this thread now that I got far enough for it to potentially turn it into a PR someday. I basically followed the approach that Keefer was proposing initially: just copy real_inner_product.lean into complex_inner_product.lean and get going. So far the result is basically what you'd expect: the awkward duplication with the real case, the lack of connection with the existing sesquilinear form code (that I only discovered when I almost done), and coded by an obvious beginner.

Anyway, in case anybody is interested, I put it on github here:
https://github.com/dupuisf/mathlib/blob/hilbert/src/analysis/normed_space/complex_inner_product.lean

[Sebastien Gouezel]

I should mention that there is a flaw in the current design of the real inner product space (you can not put an instance on reals, because this leads to two norms which are not seen as the same norm by Lean kernel, which creates a lot of issue). This is fixed in #3060.

[Frédéric Dupuis]

I just had a look -- that clears up some questions I had while writing this... In any case, it would be nice to have a plan to get to the complex case. I guess the options would be (1) basically port this fix to the code I wrote, i.e. have a complex_inner_product.lean file that mostly duplicates the real case, (2) build it on top of sesquilinear products, but still independently from the real case, or (3) try to find a suitable generalization that works for both the real and complex case. Probably (3) would be best if we could find something that's not too awkward...