Zulip Chat Archive

Stream: maths

Topic: Complex inner product


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 26 2020 at 13:04):

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

view this post on Zulip Keefer Rowan (May 26 2020 at 13:05):

@Johan Commelin So has_cinner then?

view this post on Zulip Johan Commelin (May 26 2020 at 13:05):

Well....

view this post on Zulip Reid Barton (May 26 2020 at 13:06):

Am I confusing this with something else?

view this post on Zulip Johan Commelin (May 26 2020 at 13:06):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 26 2020 at 13:07):

Maybe it was already refactored: linear_algebra.sesquilinear_form

view this post on Zulip Johan Commelin (May 26 2020 at 13:07):

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

view this post on Zulip Johan Commelin (May 26 2020 at 13:09):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 26 2020 at 13:11):

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

view this post on Zulip Johan Commelin (May 26 2020 at 13:12):

Maybe something with diagonalizing matrices

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 26 2020 at 13:14):

Ok, I don't know anything about Hilbert spaces

view this post on Zulip Johan Commelin (May 26 2020 at 13:15):

But we certainly want those

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 26 2020 at 13:16):

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

view this post on Zulip 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

view this post on Zulip Keefer Rowan (May 26 2020 at 13:17):

any ideas?

view this post on Zulip Johan Commelin (May 26 2020 at 13:17):

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

view this post on Zulip Johan Commelin (May 26 2020 at 13:17):

Does that look acceptable?

view this post on Zulip Johan Commelin (May 26 2020 at 13:18):

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

view this post on Zulip Johan Commelin (May 26 2020 at 13:18):

Because we can't do proper subscripts

view this post on Zulip Johan Commelin (May 26 2020 at 13:18):

The other option is to try the out_param thing

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 26 2020 at 13:21):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 26 2020 at 13:27):

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

view this post on Zulip Johan Commelin (May 26 2020 at 13:27):

I'm not sure though

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 26 2020 at 13:27):

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

view this post on Zulip Johan Commelin (May 26 2020 at 13:28):

And my alter ego does use bracket notation for them

view this post on Zulip 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?

view this post on Zulip Keefer Rowan (May 26 2020 at 13:37):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 26 2020 at 13:39):

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

view this post on Zulip Keefer Rowan (May 26 2020 at 13:39):

What should the class be called? has_cinner or has_innerc?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 26 2020 at 13:40):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Sebastien Gouezel (May 26 2020 at 14:13):

I can't find hermitian anywhere in mathlib.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Scott Morrison (May 26 2020 at 14:22):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 26 2020 at 14:24):

Bourbaki doesn't consider quaternionic Hilbert spaces??

view this post on Zulip Patrick Massot (May 26 2020 at 14:24):

Maybe this is a French/English translation issue

view this post on Zulip 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?

view this post on Zulip Reid Barton (May 26 2020 at 14:25):

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

view this post on Zulip Keefer Rowan (May 26 2020 at 14:27):

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

view this post on Zulip Patrick Massot (May 26 2020 at 14:28):

positive definite ones are a special case

view this post on Zulip Patrick Massot (May 26 2020 at 14:28):

In general they aren't

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 26 2020 at 14:31):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Johan Commelin (May 26 2020 at 14:43):

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

view this post on Zulip 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 F=C\mathbb{F} = \mathbb{C} or R\mathbb{R} and then you write proofs for C\mathbb{C} that also work for R\mathbb{R} (since there is an informal "coercion" RC\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.

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Scott Morrison (May 26 2020 at 16:07):

(That might be totally wrong...)

view this post on Zulip Johan Commelin (May 26 2020 at 16:09):

@Scott Morrison your suggestion requires a normed field.

view this post on Zulip Scott Morrison (May 26 2020 at 16:10):

Yes

view this post on Zulip 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.

view this post on Zulip Scott Morrison (May 26 2020 at 16:10):

There are non-normed fields?! :-)

view this post on Zulip Johan Commelin (May 26 2020 at 16:10):

Scott Morrison said:

There are non-normed fields?! :-)

Only on Wednesdays

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 26 2020 at 16:54):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 27 2020 at 01:26):

Actually even having a typeclass is_R_or_C would be a bit challenging

view this post on Zulip 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

view this post on Zulip Keefer Rowan (May 27 2020 at 01:30):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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>.

view this post on Zulip Scott Morrison (May 27 2020 at 01:35):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 27 2020 at 01:40):

something to do with quantum logic

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Keefer Rowan (May 27 2020 at 01:52):

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

view this post on Zulip 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 x,y=Ux,UyUxUy=xy|\langle x ,y \rangle | = |\langle U x, U y \rangle | \leq \| U x \| \| U y\| = \|x\| \|y\| where UU is the isometry? Perhaps many of the theorems can be recovered this way.

view this post on Zulip 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 R\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

view this post on Zulip Mario Carneiro (May 27 2020 at 02:05):

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

view this post on Zulip 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

view this post on Zulip 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 x,y=Ux,UyUxUy=xy|\langle x ,y \rangle | = |\langle U x, U y \rangle | \leq \| U x \| \| U y\| = \|x\| \|y\| where UU 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 27 2020 at 05:37):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 27 2020 at 06:02):

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

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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Mario Carneiro (May 27 2020 at 06:19):

/me wonders which meaning of "real" Scott meant

view this post on Zulip 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+igf+ig), then apply the complex result, then use the fact that the original inner product was real.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Scott Morrison (May 27 2020 at 11:52):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 27 2020 at 11:53):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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