Topological vector spaces

[mkerjean]

Motivation for this change

Adding topological vector spaces as a new structure. Further PRs will integrate the theory of topological vector spaces (duality, function spaces, characterization of topologies, distribution theory)

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[mkerjean]

For the record, a previous comment on PR#539, now closed by @zstone1 "With a long-term goal of doing spectral theory, I'm looking at defining integrals for a TVS. The most straightforward choice seems to be "weak integrals"."

[affeldt-aist]

The last commit makes the dev compile but it is clearly a temporary fix.

[zstone1]

Mostly looks great. A few renamings, a few nitpicks. And I know you're already on top of the duplication with resepct to normedtype.v.

The only one I think is blocking is removing the "lawless joins" between Filtered/nbhs/topological + modules. I wouldn't care so much if structures could be declared locally. But globally adding these structures seems like something we'll regret later. If approach doesn't work, let me know and we can figure out something else.

[zstone1]

Nitpicks: since HB has rather strong requirements that

• you can't define joins twice
• you must define joins "bottom-up" in the hierarchy

It's a bit more forward-compatible to define in the earliest places they can. The Pointed + something from mathcomp can live next to pointed.

[mkerjean]

Thanks for the suggestion, I'll make the change and resolve the conversation when done.

[zstone1]

Note: In topology.v we have

HB.instance Definition _ (R : zmodType) := isPointed.Build R 0.

which conflicts with this structure. I'm not sure if it will matter in practice, and honestly I'm not even sure why we have that instance in topology.v at all. If we could safely remove that from topology that would be great. Mostly this is a heads up that this structure has bad inheritance paths.

[zstone1]

To resolve before merge: Having these joins without the natural compatibility mixins (AKA continuity) concerns me a bit. Since these things have a uniform structure anyway, doing it with the TopologicalLmod_isTvs factory makes a lot sense. But I also see that you use nbhs0N_subproof twice, and these structures are useful for refactoring that.

I think there is an alternative that get best of both worlds. I'm not sure if this is the "right way" to do it, but a viable approach is to take the group structure as an extra argument:

Section properties_of_topologicallmodule.
Context (R : numDomainType) (E : topologicalType) 
    (Me : GRing.Lmodule R E) (U : set E).
Let ME := GRing.Lmodule.Pack Me.

Lemma nbhsN_subproof (f : continuous (fun z : R^o * E => z.1 *: (z.2 : ME))) (x : E) :
  nbhs x U -> nbhs (-(x:ME)) (-%R @` (U : set ME)).
Proof.
move => Ux; move: (@f (-1,-(x:ME)) U); rewrite /= scaleN1r opprK => /(_ Ux) [] /=.
move => [B] B12  [B1 B2] BU; near=> y; exists (-(y:ME)); rewrite ?opprK -?scaleN1r //.
apply: (BU (-1,y)); split => /=; last by near:y; rewrite nearE.
by move: B1 => [] //= ? ?; apply => [] /=; rewrite subrr normr0.
Unshelve. all: by end_near. Qed.

Then when E has a lmodule structure, you use GRing.Lmodule.class E to extract it. So you have to add a few extra annotations, but this quirk is hidden inside these subproof lemmas. I haven't tried this all the way, so I can't confirm yet that it will actually 100%, but I'm optimisitc

[mkerjean]

Adding your solution within the section properties_of_topologicallmodule, with a few 0 : E to be specified in the factory TopologicalLmod_isTvs , in the sense that the Pointed/Filtered + N/z/Lmodules instances can be deleted. The following joins, involving Nbhs, Topological and Uniform, are still necessary. Is this still an issue? Is there a way to define these joins locally?

[zstone1]

I'm a little confused why they are necessary? The file does build (on my machine) without those joins. Is there a result you have in mind that relies one of the lawless joins? If they are necessary then that's fine, but if they can be removed that would be better.

[mkerjean]

On my machine normedtype.v does not build when the modification is done to tvs.v, as there is an issue for the definition of PseudoMetricNormedZmod (l. 255). Taking out the Uniform + Lmodule join gives the following error message:

You must declare the hierarchy bottom-up or addd a missing join. 
There are two ways out: 
- declare structure PseudoMetricNormedZmod before structure Tvs if Tvs inherits from it; 
- declare an additional structure that inherits from both Uniform and GRing.Zmodule and from which PseudoMetricNormedZmod and/or Tvs inherit.

I have to say it's unclear to me why taking out the pointed and filtered joins does not create an issue like this one.

[zstone1]

Ah! I see what's happening here. You're right, it does seem hopeless to remove these. Sorry for sending you down a rabbit hole!

[pi8027]

Context (R : numDomainType) (E : topologicalType) 
    (Me : GRing.Lmodule R E) (U : set E).
Let ME := GRing.Lmodule.Pack Me.

@zstone1 @mkerjean @Tragicus This proof does not work since coq/coq#19611 because GRing.Lmodule.sort ME no longer triggers canonical structure inference and gets reduced immediately. Can't we just use the TopologicalLmodule structure instead?

[mkerjean]

I'm fine with it, but I would like @zstone1's confirmation as he suggested the change. See also @Tragicus's comment on PR#1402.

[zstone1]

Yeah, it's fine with me. If we have to have topologicalLmodule anyway, we might as well use it.

[affeldt-aist]

There are a few comments in this PR that point at code duplication; just after it is merged, I think it would be good to open an issue with links to duplications so that they can be taken care of later.
I think that I already asked, but in the section prod_NormedModule, numDomainType gets specialized to numFieldType: is it unavoidable? (I remember that I double-checked myself and got to the conclusion that it is but I do not remember precisely.)
The commented HB.structure at the top of the type tvs.v can maybe be deleted.
@CohenCyril, do you see anything potentially problematic?

[mkerjean]

Rebasing the branch over mc-analysis 1.6.0, and in particular over the PR splitting topology in multiple files, makes the compilation fail. real.v does not find the splitted files when importing the topology. This seems to work in master on the CI. What is missing in the branch evt2?

[affeldt-aist]

Rebasing the branch over mc-analysis 1.6.0, and in particular over the PR splitting topology in multiple files, makes the compilation fail. real.v does not find the splitted files when importing the topology. This seems to work in master on the CI. What is missing in the branch evt2?

I am not sure but that maybe because you have some Require Imports that do not start with From mathcomp even though the latter has been made mandatory by the use the -Q option instead of -R introduced by the PR 1348.

[zstone1]

I encountered a possibly similar issue where a stray .vo file confusing the build. Doing a make clean doesn't remove .vo that correspond to deleted .v files. So you might still have theories/topology.vo that must be deleted manually.

[proux01]

In such cases, I tend to use git clean -dxf . (be sure to check the output of the dry run git clean -dxn . before)

[proux01]

\o/