analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
A somewhat dramatic change in how things are organized. This breaks topology into a folder with a bunch of files in it. This has two big benefits - Dependencies are...
##### Motivation for this change fixes #1358 fixes #1359 ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` ~~- [ ] added corresponding documentation in the headers~~ Reference: [How to...
Co-authored-by: @jmmarulang ##### Motivation for this change Addresses issue #1360 ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [x] added corresponding documentation in the headers Reference: [How to...
This code could be generalized to extended reals without much issues, it seems that not much depends on these definitions https://github.com/math-comp/analysis/blob/6dfceaafefdeace2147a1ad9a307223641dccdb1/theories/measure.v#L5250C1-L5266C24 @jmmarulang
```coq From HB Require Import structures. From mathcomp Require Import all_ssreflect. From mathcomp Require Import all_fingroup. From mathcomp Require Import lebesgue_integral. ``` fails with error ``` Error: Notation "_ \x...
```coq From HB Require Import structures. From mathcomp Require Import all_ssreflect. From mathcomp Require Import all_fingroup. From mathcomp Require Import all_algebra. From mathcomp Require Import all_solvable. From mathcomp Require Import...
A grab-bag of results I'll need to split into separate reviews (once topology.v's split is done). This PR is mostly for bookkeeping, and stating my (new) roadmap for homotopies. My...
https://github.com/math-comp/analysis/blob/a413c3f01752b9cc6223fd5457c22e2dde944165/theories/sequences.v#L945 `: V` is not needed anymore @proux01
We already have proofs about curry/uncurry which require locally compact and uniform. One one hand, these results are critical for homotopy theory. One the other hand they are badly phrased...
In theories/normedtype.v ```Coq (* Ideally, R should be an instance of realType here, rather than a section variable. *) ``` C.f. https://github.com/math-comp/analysis/pull/1347
