math-comp
Tvs and duality theory
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.
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?
