[Merged by Bors] - feat(analysis/normed_space/inner_product): Define the inner product based on is_R_or_C

[dupuisf]

---

This PR redefines the inner product to be based on the is_R_or_C typeclass. Its API is very close to the original one, and whenever a lemma has a cleaner statement in the real case (i.e. if it contains things like re or conj), there is a specialized lemma for that case. The plan would be to then replace real_inner_product.lean by this (which I haven't done yet here). I have ported the rest of mathlib to this new inner product and deleted real_inner_product.lean.

A few things worth noting:

• The naming scheme: I would suggest replacing names like inner_smul_left by inner.smul_left, with the real and complex cases as inner.real.smul_left and inner.complex.smul_left. I have now switched to just keeping the same naming scheme, with inner replaced with real_inner in a lemma name whenever the lemma only applies to the real inner product, or else tagging _real at the end of the name if inner doesn't appear in the lemma name.
• The linter complains about a dangerous instance for to_normed_group, because one gets a free parameter. It seems to be local only to this file though, unless I'm misinterpreting what local attribute means.
• The copyright notice: I just took the notice from real_inner_product and added myself in the list of authors, since a large part of it was copy/pasted from there. If this is inappropriate, please let me know.

[sgouezel]

This looks very good to me. My only real question is about the projection part: my impression is that it only needs to be done over the reals, and then it should automatically become available over the complexes thanks to suitable instances.

[sgouezel]

There is a difficulty here that, when you write inner x y, Lean can not guess the field. If you have a (complex) hermitian vector field, and you derive the real inner product space structure, then you will have two different inner spaces on it and Lean will get confused. You have a nice solution below, by introducing the notations ⟪x, y⟫_ℝ and ⟪x, y⟫_ℂ. I think it is worth moving these notations just after the definition and making them global. Also, introducing localized notations for ⟪x, y⟫ as you have done at the end of the file is very good, but you could move them right here. And you could also introduce a third locale inner_product_space where the field is unspecified, and left to Lean. Then the user could choose which locale he wants to open depending on the context. (In this file, you would want to open inner_product_space, for instance) (Maybe you will need to declare the notations in a section, to avoid them being open automatically in the whole file)

[dupuisf]

I made the ⟪x, y⟫_ℝ and ⟪x, y⟫_ℂ declarations global and moved the rest of the notations up here, but for the inner_product_space localized notation, I suspect that if this is needed elsewhere, one would want to do what I did here: first declare 𝕜 to be some is_R_or_C field, and then declare ⟪x, y⟫ to be the inner product with this specific 𝕜 as the field. I had tried leaving it unspecified and it caused problems.

[sgouezel]

You shouldn't need normed_space ℝ α here. Instead, you should have an instance from normed_space k α to normed_space ℝ α. Or, better, just formulate the theorem for real vector spaces, and let restrict_scalars automatically handle the complex case for you (you would need an instance that a complex inner product space is also a real inner product space, which is good to have in any case)

[dupuisf]

I actually ran into annoying problems when trying to define these kinds of instances (where is_R_or_C implies real). If I try to declare, for example, that semimodule 𝕜 α implies semimodule ℝ α, Lean complains about the case where 𝕜 = ℝ, because then this new instance is not defeq to the original one. I have no idea how to solve this -- if you have any ideas that would be great!

[sgouezel]

What about just having an instance that inner_product_space C alpha implies inner_product_space R alpha? And stating all the projection theorems only in real inner product spaces. Then they would also become automatically available in complex inner product spaces as well (since they are just a statement about the norm), which should be enough for applications.

[dupuisf]

I added the instance (it certainly can't hurt!), but I think it would still be good to prove these for the is_R_or_C case directly, because once we split into two cases, we're condemned to also split everything that gets built on top...

[sgouezel]

I don't agree with you here: this projection business is specifically a real thing (it requires convexity of the set, which only makes sense in a real context), so it should only be stated for real vector spaces.

The version that would make sense for any is_R_or_C field 𝕜 is that, for any 𝕜-subspace, there is a unique projection on 𝕜 minimizing the distance (which can be stated using only the distance, so not mentioning reals at all). And if you can find properties on the scalar product that only mention 𝕜, then they are worth stating in this context.

So, my suggestion is:

• Do all the projection business with convex subsets, and everything that mentions ℝ, in a specific section that does not mention any field 𝕜
• Then deduce the results that make sense over any is_R_or_C field (and that don't mention ℝ at all) in another section, by registering locally an instance that the space is also a real inner product space, and using the previous results for real inner product spaces. This instance would be a bad instance as you mention (as for 𝕜 = ℝ is creates non-defeq instances) but if it is just a local instance specific to these proofs this is not an issue.

If you don't see how to do this, I can have a go at it if you like.

[dupuisf]

Ah I see -- alright I'll give it a shot!

[dupuisf]

This isn't going too well. That instance does really strange things, even locally (abel stops working in random places, the typeclass system goes nuts on things like semiring ℝ in some of these statements, etc). Now I just rewrote that whole section to just be for real inner products and left the instance unused -- feel free to have a shot at it though.

[sgouezel]

The trick is to not register this as an instance (even not a local one), but only to use it in proofs to declare explicitly the real structure on a given space, with letI. This means that Lean will not try the instance on this real structure, so nothing bad will happen.

I have done this, and everything went pretty well! Now, the only thing that is specific to real spaces is the projection on convex sets. Orthogonal projection on complete subspaces is done in the general setting of an is_R_or_C field (and I had nothing to change to the proofs, so it definitely convinced me that this is a really efficient way to do things at the same time on reals and complexes!)

It looks ready for merging to me, but before I can merge it someone should have a look to the changes I have made in my last commit. Can you check that you're happy with what I've done?

[dupuisf]

I'm certainly happy with it for what it's worth -- thanks a lot!

[kim-em]

This looks really good! I'm happy that the is_R_or_C typeclass is working out.

I'm going to mark this again as awaiting-author so @dupuisf can review @sgouezel's last changes, but I think this is getting very close to merging now.

[sgouezel]

bors r+
Thanks!

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests