math-comp / analysis

Mathematical Components compliant Analysis Library
Other
200 stars 44 forks source link

Topological vector spaces #1300

Open mkerjean opened 1 month ago

mkerjean commented 1 month ago
Motivation for this change

Adding the theory of topological vector spaces

Checklist

Reference: How to document

Reminder to reviewers
mkerjean commented 1 month ago

If I understand correctly, the evt2 branch still depends on the old hierarchy builder branch and not on the master branch which is now ported to hierarchy builder, hence the MC2 label.

mkerjean commented 1 month ago

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 commented 3 weeks ago

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