analysis

analysis copied to clipboard

The most technical of all the parts of #1350. This proves that path concatenation has left/right identities, and associates, up to reparameterization. The current proofs are slow, ugly, and ill-named....

zstone1

##### Motivation for this change This change introduces the weighted probability distribution `wgt` ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [x] added corresponding documentation in the headers...

hoheinzollern

Lemmas `fiberwise_{finite,countable}_preimage`

1

##### Motivation for this change Add lemmas stating that the preimage of a set along a function is finite / countable if every pointwise preimage is so. NB: there is...

t6s

```coq Lemma cvg_dnbhs_at_right (f : R -> R) (p : R) (l : R) : f x @[x --> p^'] --> l -> f x @[x --> p^'+] --> l....

affeldt-aist

Generalize integration_by_parts

6

##### Motivation for this change Add a part of generalized version of integration by parts for unbound intervals `` `[a, +oo[ ``. This PR is over #1656 and #1662. I...

IshiguroYoshihiro

##### Motivation for this change ##### Checklist - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding documentation in the headers Reference: [How to document](https://github.com/math-comp/math-comp/wiki/How-to-document) ##### Merge...

affeldt-aist

adherence value, extracted seq, limit point

4

##### Motivation for this change ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [x] added corresponding documentation in the headers Reference: [How to document](https://github.com/math-comp/math-comp/wiki/How-to-document) ##### Merge policy As...

affeldt-aist

##### Motivation for this change missing lemme about `integrable` and `norm` @holgerthies @IshiguroYoshihiro ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` ~~- [ ] added corresponding documentation in the...

affeldt-aist

Lemmas `interval_set1` and `set_itv1` have identical statements. https://github.com/math-comp/analysis/blob/eed79156fac45c0aaa5d37aa047e89dbf4481f9c/classical/set_interval.v#L123 https://github.com/math-comp/analysis/blob/eed79156fac45c0aaa5d37aa047e89dbf4481f9c/classical/set_interval.v#L141

IshiguroYoshihiro

Normed vector types, infinite norm, norm equivalence thm, continuity …

3

Continuity of linear functions in finite dimension ##### Motivation for this change ##### Checklist - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding documentation in the...

Tragicus