Marie Kerjean
Marie Kerjean
After PR[#267](https://github.com/math-comp/analysis/pull/267) is merged, should we add to `landau.v` lemmas about bounded functions using landau notations ? [This](https://github.com/math-comp/analysis/blob/309f5131169a15542e29d9e55a0ee23a2bb67862/theories/banachsteinhaus.v#L219) is needed for Banach-Steinhauss for example. NB(rei): PR #267 has been closed...
In `derive.v`, we should formalize the theorem that derive + continuous partial derivatives implies differentiability
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...
This is in beginner's style and should heavily rewritten. It contains two files: - `hahnbanach.v` contains a new formalization of Zorn's Lemma depending of the Choice in Prop and to...
A proof of Baire and Banach-Steinhaus theorem, initiated by Theo Vignon. Waiting for [PR#183](https://github.com/math-comp/analysis/pull/183) to be merged to rebase on master.
##### Motivation for this change Adding the theory of topological vector spaces ##### Things done/to do - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding documentation...
##### 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...
`Normedmodtype.v` is a long file, and this triggers several issues, alike the one descripe in [Issue#1167](https://github.com/math-comp/analysis/issues/1167) advocating the spit of `topology.v`. - Compilation takes a long time, when trying to...