analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
https://github.com/math-comp/analysis/blob/c5ea0abfda9c1ec4f223ea2e013de20fbf23135f/theories/hoelder.v#L86 Try to change this lemma to have no condition when enabling ``` (mu (f @^-1` (setT `\ 0%R))) ``` when `p = 0` (which looks like a saner convention...
##### 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...
https://github.com/math-comp/analysis/blob/2f645cfffd5ee1c8abfda6f8deee2110af0c1db7/theories/probability.v#L151-L152 `cdf` should be made an instance of `Cumulative` (from `lebesgue_stieltjes_measure.v`), however functions in `Cumulative` have codomain `R` whereas `cdf` expects codomain `\bar R. It should be generalized to topological...
##### Motivation for this change I add `Section cdf_of_lebesgue_stieltjes_mesure` in `probability.v`, which proves that the cumulative distribution function of a Lebesgue-Stieltjes measure goes back to the underlying function. ##### Checklist...
##### Motivation for this change Resurrection of https://github.com/math-comp/analysis/pull/204. fyi: @mkerjean ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [x] added corresponding documentation in the headers Reference: [How to...
https://github.com/math-comp/analysis/blob/3cd35520dc1d14ef272e2c6a25f41a94582ab041/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v#L368
In `probability.v`, I would like to rewrite the function under `cvg_to` by ``` eq_cvg : forall (T T' : Type) (F : set_system T) (f g : T -> T')...
https://github.com/math-comp/analysis/blob/05898dcecc81e696b04dde8883718d54f2109990/theories/normedtype_theory/num_normedtype.v#L2 num_normedtype.v improted HB, but does not use HB.
##### Motivation for this change The same simplification should apply to (most of) the following lines: ``` $ grep -n --color '\(subrr add\(0r\|r0\)\|div\(rr\|ff\) ?mul\(1r\|r1\)\)' $(git ls-files | grep '\.v$') theories/convex.v:217:...
##### Motivation for this change fyi @mkerjean (application of Baire) @IshiguroYoshihiro ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [x] added corresponding documentation in the headers Reference: [How...