# Zulip Chat Archive

## Stream: maths

### Topic: Complex inner product

#### Keefer Rowan (May 26 2020 at 12:57):

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 (May 26 2020 at 13:02):

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 (May 26 2020 at 13:03):

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

#### Keefer Rowan (May 26 2020 at 13:04):

@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 (May 26 2020 at 13:04):

@Reid Barton `git grep inner`

doesn't show anything interesting outside `real_inner_product.lean`

#### Keefer Rowan (May 26 2020 at 13:05):

@Johan Commelin So `has_cinner`

then?

#### Johan Commelin (May 26 2020 at 13:05):

Well....

#### Reid Barton (May 26 2020 at 13:06):

Am I confusing this with something else?

#### Johan Commelin (May 26 2020 at 13:06):

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

#### Johan Commelin (May 26 2020 at 13:07):

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

#### Reid Barton (May 26 2020 at 13:07):

Maybe it was already refactored: `linear_algebra.sesquilinear_form`

#### Johan Commelin (May 26 2020 at 13:07):

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

#### Johan Commelin (May 26 2020 at 13:09):

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

#### Johan Commelin (May 26 2020 at 13:11):

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

#### Johan Commelin (May 26 2020 at 13:11):

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

#### Johan Commelin (May 26 2020 at 13:12):

Maybe something with diagonalizing matrices

#### Keefer Rowan (May 26 2020 at 13:13):

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 (May 26 2020 at 13:14):

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

#### Johan Commelin (May 26 2020 at 13:14):

Ok, I don't know anything about Hilbert spaces

#### Johan Commelin (May 26 2020 at 13:15):

But we certainly want those

#### Keefer Rowan (May 26 2020 at 13:15):

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 (May 26 2020 at 13:15):

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

#### Johan Commelin (May 26 2020 at 13:16):

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

#### Keefer Rowan (May 26 2020 at 13:17):

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 (May 26 2020 at 13:17):

any ideas?

#### Johan Commelin (May 26 2020 at 13:17):

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

#### Johan Commelin (May 26 2020 at 13:17):

Does that look acceptable?

#### Johan Commelin (May 26 2020 at 13:18):

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

#### Johan Commelin (May 26 2020 at 13:18):

Because we can't do proper subscripts

#### Johan Commelin (May 26 2020 at 13:18):

The other option is to try the `out_param`

thing

#### Keefer Rowan (May 26 2020 at 13:20):

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 (May 26 2020 at 13:20):

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 (May 26 2020 at 13:21):

@Sebastien Gouezel But that would be `restrict_scalars real complex V`

, right?

#### Keefer Rowan (May 26 2020 at 13:25):

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 (May 26 2020 at 13:27):

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

#### Johan Commelin (May 26 2020 at 13:27):

I'm not sure though

#### Sebastien Gouezel (May 26 2020 at 13:27):

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 (May 26 2020 at 13:27):

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

#### Johan Commelin (May 26 2020 at 13:28):

And my alter ego does use bracket notation for them

#### Johan Commelin (May 26 2020 at 13:31):

@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 (May 26 2020 at 13:37):

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

#### Sebastien Gouezel (May 26 2020 at 13:37):

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 (May 26 2020 at 13:39):

So separate classes, and ignore fields that aren't `real`

or `complex`

.

#### Keefer Rowan (May 26 2020 at 13:39):

What should the class be called? has_cinner or has_innerc?

#### Sebastien Gouezel (May 26 2020 at 13:40):

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

#### Johan Commelin (May 26 2020 at 13:40):

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

#### Patrick Massot (May 26 2020 at 14:09):

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 (May 26 2020 at 14:11):

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 (May 26 2020 at 14:13):

I can't find `hermitian`

anywhere in mathlib.

#### Keefer Rowan (May 26 2020 at 14:18):

@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 (May 26 2020 at 14:21):

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 (May 26 2020 at 14:22):

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

#### Scott Morrison (May 26 2020 at 14:23):

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 (May 26 2020 at 14:24):

Bourbaki doesn't consider quaternionic Hilbert spaces??

#### Patrick Massot (May 26 2020 at 14:24):

Maybe this is a French/English translation issue

#### Patrick Massot (May 26 2020 at 14:25):

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

#### Reid Barton (May 26 2020 at 14:25):

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

#### Keefer Rowan (May 26 2020 at 14:27):

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

#### Patrick Massot (May 26 2020 at 14:28):

positive definite ones are a special case

#### Patrick Massot (May 26 2020 at 14:28):

In general they aren't

#### Scott Morrison (May 26 2020 at 14:28):

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 (May 26 2020 at 14:29):

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 (May 26 2020 at 14:30):

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

#### Scott Morrison (May 26 2020 at 14:30):

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

#### Johan Commelin (May 26 2020 at 14:31):

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

#### Johan Commelin (May 26 2020 at 14:31):

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 (May 26 2020 at 14:32):

Shouldn't we define `innerc_product_space`

as usual and then prove it is an instance of a sesquilinear form?

#### Scott Morrison (May 26 2020 at 14:32):

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 (May 26 2020 at 14:35):

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

#### Scott Morrison (May 26 2020 at 14:35):

@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 (May 26 2020 at 14:36):

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 (May 26 2020 at 14:37):

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

#### Scott Morrison (May 26 2020 at 14:38):

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 (May 26 2020 at 14:43):

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

#### Keefer Rowan (May 26 2020 at 15:29):

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 (May 26 2020 at 16:07):

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 (May 26 2020 at 16:07):

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

#### Scott Morrison (May 26 2020 at 16:07):

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

#### Johan Commelin (May 26 2020 at 16:07):

Do you need that `R`

is totally ordered? Or is it enough to have a notion of positive elements?

#### Scott Morrison (May 26 2020 at 16:07):

(That might be totally wrong...)

#### Johan Commelin (May 26 2020 at 16:09):

@Scott Morrison your suggestion requires a normed field.

#### Scott Morrison (May 26 2020 at 16:10):

Yes

#### Johan Commelin (May 26 2020 at 16:10):

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

#### Scott Morrison (May 26 2020 at 16:10):

There are non-normed fields?! :-)

#### Johan Commelin (May 26 2020 at 16:10):

Scott Morrison said:

There are non-normed fields?! :-)

Only on Wednesdays

#### Johan Commelin (May 26 2020 at 16:53):

@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 (May 26 2020 at 16:54):

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

#### Keefer Rowan (May 27 2020 at 01:25):

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 (May 27 2020 at 01:26):

Actually even having a typeclass `is_R_or_C`

would be a bit challenging

#### Mario Carneiro (May 27 2020 at 01:28):

it's probably easier to define `is_R_or_C`

to mean "having all the common identities we want" like polarization

#### Keefer Rowan (May 27 2020 at 01:30):

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

#### Mario Carneiro (May 27 2020 at 01:31):

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

#### Mario Carneiro (May 27 2020 at 01:32):

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 (May 27 2020 at 01:34):

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 (May 27 2020 at 01:35):

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 (May 27 2020 at 01:35):

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

#### Mario Carneiro (May 27 2020 at 01:37):

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 (May 27 2020 at 01:37):

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 (May 27 2020 at 01:39):

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 (May 27 2020 at 01:40):

something to do with quantum logic

#### Mario Carneiro (May 27 2020 at 01:42):

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

#### Mario Carneiro (May 27 2020 at 01:47):

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

#### Mario Carneiro (May 27 2020 at 01:48):

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 (May 27 2020 at 01:52):

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

#### Keefer Rowan (May 27 2020 at 01:59):

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 (May 27 2020 at 02:04):

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 (May 27 2020 at 02:05):

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 (May 27 2020 at 02:06):

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 (May 27 2020 at 02:09):

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 (May 27 2020 at 05:29):

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 (May 27 2020 at 05:35):

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 (May 27 2020 at 05:36):

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

#### Mario Carneiro (May 27 2020 at 05:37):

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

#### Mario Carneiro (May 27 2020 at 05:40):

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 (May 27 2020 at 05:45):

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 (May 27 2020 at 05:56):

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 (May 27 2020 at 06:02):

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 (May 27 2020 at 06:03):

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

#### Yury G. Kudryashov (May 27 2020 at 06:16):

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

#### Mario Carneiro (May 27 2020 at 06:19):

/me wonders which meaning of "real" Scott meant

#### Yury G. Kudryashov (May 27 2020 at 06:23):

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 (May 27 2020 at 06:25):

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 (May 27 2020 at 06:25):

And then we can bicker about what the weakest assumptions on a `is_R_or_C`

class should be.

#### Keefer Rowan (May 27 2020 at 11:47):

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 (May 27 2020 at 11:48):

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 (May 27 2020 at 11:50):

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 (May 27 2020 at 11:52):

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

#### Kevin Buzzard (May 27 2020 at 11:52):

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

#### Scott Morrison (May 27 2020 at 11:52):

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 (May 27 2020 at 11:53):

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

#### Frédéric Dupuis (Jun 14 2020 at 02:21):

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 (Jun 14 2020 at 07:34):

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 (Jun 15 2020 at 03:52):

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...

Last updated: May 06 2021 at 19:30 UTC