Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Tvs and duality theory #539

Closed
wants to merge 5 commits into from
Closed

Tvs and duality theory #539

wants to merge 5 commits into from

Conversation

mkerjean
Copy link
Collaborator

@mkerjean mkerjean commented Feb 8, 2022

Duality theory in topological vector spaces.

This is work in slow progress, submitted as a PR to allow potential discussions with other ongoing works.
The goal is to prove Mackey-arens theorem and characterization of reflexive spaces in terms
of barrelledness and weak quasi-completeness, while allowing symmetric notations and computations
between a reflexive topological vector space and its dual.
It will allow generalization of Hahn-Banach PR337 and Banach-Steinhaus PR334 theorems, and make use of functions spaces as defined in topology.v. Once this PR is merged, it will allow to move to metric spaces and distribution theory.
As normedModules are specific instances of tvs, some refinement and simplifications will appear in normedtype.v.

@mkerjean mkerjean marked this pull request as draft February 8, 2022 15:15
@mkerjean mkerjean force-pushed the dual branch 4 times, most recently from 4ec07c5 to 61708a9 Compare February 11, 2022 21:34
@zstone1
Copy link
Contributor

zstone1 commented Jun 25, 2022

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". I can work in a normed vector space for now, but I'd love to build on your work directly. What is the state of this PR today? And is there anything I can do to help get it ready for submission?

@proux01 proux01 added the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Jan 25, 2024
@mkerjean
Copy link
Collaborator Author

mkerjean commented Sep 5, 2024

Closed as PR#1300 subsumes it with the use of HB.

@mkerjean mkerjean closed this Sep 5, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants