feat(analysis/locally_convex): the topology of a locally convex space is generated by seminorms

[mcdoll]

This PR provides the proof that every locally convex space has a family of seminorms that induces the topology.

This PR also adds a new simp-lemma is_R_or_C.real_norm, which calculates the norm of a real number r coerced into a is_R_or_C type as the norm of r. This made it necessary to change some proofs in a few places.

---

• [x] depends on: #14879

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#14879~~ By Dependent Issues (🤖). Happy coding!

[ocfnash]

bors d=ADedecker

[bors[bot]]

:v: ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ADedecker]

I am really sorry for leaving that rotting for a month, it got lost into my chaotic todo list for the beginning of the year.

Your last comment about all continuous seminorms being gauge of absolutely convex open sets made me think about an alternative approach, which you can see on the branch AD_disks_tmp. Essentially, I tried working directly with all continuous seminorms and, modulo some useful prerequisites which I have PR-ed in the mean time, it turned out to be shorter. I think we should have both statements anyway, so the question is simply which do we prove first.

Another thing that would be nice is to get something stronger than just having a family of seminorms. Namely, it would be useful to know that if we have a neighborhood basis of zero indexed by \iota, then we can also get a family of seminorms indexed by \iota (this will be especially useful for \iota = \N). I think this should be easy to get from both approaches. I think this can wait for another PR, but we should keep that in mind when choosing between your approach and mine.

I would just like to get your opinion in these two points, otherwise the PR looks good to me.

(Btw, there are conflicts now. Sorry again for the delay!)

[mcdoll]

It is well-known that you can prove this by showing stuff about continuous seminorms (this is for instance done in Narici-Beckenstein). My reason for not doing that way was that I don't see any immediate application for continuous seminorms (I don't think I ever use continuity in applications - this is not to say that it is not possible, I am certain that there are results that have very fancy proofs when using that the seminorms are continuous). On the other hand, we need absolutely convex sets for certain and I thought that even if I don't prove that much about them (mainly the fact that the convex hull of a balanced set is balanced and that they form a basis of the filter).

As for the index set: that is true, I mentioned that in some other PR (where I proved that converse direction: countable seminorms implies first countable topology). I also think that this not in the scope for this PR. One addition that would be useful is that if you have a neighborhood basis, then taking the convex hull of the balanced core of each element in the basis yields again a basis, which implies your statement, but I don't have too much time at the moment and if you want to prove your statement with the continuous seminorms please go ahead.

[ADedecker]

Okay if you think the absolutely convex approach will be useful anyway, let's merge this (I'll fix the build error). It shouldn't be too hard to swap one approach for the other in the future anyway if we ever need it. I'll just make a quick PR proving the continuous seminorm version from this one because I will need this, and add a TODO about preserving the cardinality of the basis.

I have one last question, but I won't block the PR for that. Given that absolutely convex sets are useful for other things, is it worth making it a proper definition and providing some really basic API (like what you do for abs_convex_open_sets) just to be able to write clearer projections than h.2.2.1? :sweat_smile:

[mcdoll]

I am not sure whether we want to have a definition for absolutely convex sets. It is only two properties, but on the other side barrels need additionally need absorbing and closed. For some of the bornological space nonsense one needs absorbing absolutely convex sets. There are also different characterizations of absolutely convex sets, but I don't know how useful they are in practice. If we really need those, then I would be inclined to add a definition. Otherwise I think the main advantage of adding the definition would be that it makes things more readable and this is not very strong argument for a new definition.

[ADedecker]

Ok, I'm convinced! Let's wait for CI to finish and then I'll merge it (I don't think I can delegate further).

[ADedecker]

bors r+

[bors[bot]]

Build failed (retrying...):

• Lint mathlib

[bors[bot]]

Build failed (retrying...):

• Lint mathlib

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests