analysis

analysis copied to clipboard

change inequality in ereal_{d,}nbhs and {p,n}infty_{d,}nbhs

3

- from strict to large - also adds a few lemmas to `ereal.v` closed #122 @CohenCyril This is globally getting a bit bigger (only a few proofs are shortened). I...

affeldt-aist

Redundancies between `realseq.v` and `sequences.v`

3

There are redundancies between `altreals/realseq.v` (which predates MathComp-Analysis) and the newer `sequences.v`. How should we factorize? Related issue: "The merge of sequences and sums over general sets (see `esum.v` and...

affeldt-aist

naming in `classical_sets` conflicts with `fintype`

1

Think of a naming scheme a la `finmap`?

affeldt-aist

floor and ceil to be subsumed by MathComp

1

TODO: revise the use of floor and ceil once ~~math-comp/math-comp#682 is merged into MathComp~~ requiring MC >= 2.1.0

affeldt-aist

`finSubCover` lacks documentation

1

https://github.com/math-comp/analysis/blob/22bb6cc4adc629f47b4ec03ef38eb2138ed2c9a5/theories/topology.v#L3013-L3016

affeldt-aist

Lebesgue Stieltjes measure

1

##### Motivation for this change This is an attempt at generalizing `lebesgue_mesure.v`. RFC, FYI @hoheinzollern @IshiguroYoshihiro We have only replayed the first part so far and plan to work on...

affeldt-aist

##### Motivation for this change ##### Things done/to do - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` (do not edit former entries, only append new ones, be careful: merge and...

CohenCyril

trying to generalize mfun

1

##### Motivation for this change @CohenCyril would fix issue #662 ##### Things done/to do - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding documentation in the...

affeldt-aist

https://github.com/math-comp/analysis/blob/9d80a0fbeeaa079a930c436d3d5dbb878491cf73/theories/lebesgue_measure.v#L829-L830 Removing ` : set R` causes a stack overflow that is not explained yet. There are more instances below in the file. For the record. @CohenCyril @gares

affeldt-aist

Tvs and duality theory

1

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...

mkerjean