analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
##### Motivation for this change a sampling theorem ##### Checklist - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding documentation in the headers Reference: [How to...
Missing lemma from `@ball subspace` to the definition of `subspace_ball`
https://github.com/math-comp/analysis/blob/e00d6f76e4ddbd7bc098e0bc9c99f763e07861fd/theories/lebesgue_integral.v#L2825 should be `ge0_integral_measure_add` https://github.com/math-comp/analysis/blob/e00d6f76e4ddbd7bc098e0bc9c99f763e07861fd/theories/lebesgue_integral.v#L2640 should be `ge0_integral_pushforward`
non-homogeneous naming: ```coq inf_lower_bound: forall [R : realType] [E : set R], has_inf E -> lbound E (inf E) inf_lb: forall [R : realType] [E : set R], has_lbound E...
`measure.v` defines the following: ```coq Definition setD_closed := forall A B, B ` G A -> G B -> G (A `\` B). Definition setDI_closed := forall A B, G...
##### Motivation for this change This PR introduces an identifier for the completed lebesgue measure and a proof that the completed sigma-algebra is the same as the Caratheodory one. #####...
##### Motivation for this change ##### Checklist - [x] 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) ##### Reminder to...
##### Motivation for this change the proof is obtained by exploiting the symmetry between `at_left` and `at_right` proof used in work in progress by @IshiguroYoshihiro ##### Checklist - [x] added...
##### Motivation for this change fixes #330 ##### 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) ##### Reminder...