Commit 2020-03-23 11:21 5b2c9521
View on Github →feat(analysis/convex.cone): prove M. Riesz extension theorem, Hahn-Banach theorem (#2120)
- feat(analysis/convex.cone): prove M. Riesz extension theorem WIP
- Complete the proof
TODO: move many facts to
linear_algebra/basic
, fix possible build failures in other files - Fix compile of
analysis/convex/cone
- Cleanup, rewrite using
linear_pmap
s - Deduce Hahn-Banach theorem from M. Riesz extension theorem
- Fix lint
- Apply suggestions from code review [skip_ci] Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
- Expand comments, prove properties of
convex.to_cone
. - Docstrings
- Apply suggestions from code review Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
- Update src/analysis/convex/cone.lean
- Update src/linear_algebra/basic.lean