analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
Two related things. Now that pointed is gone from `topology`, we can canonically add topology/uniform/pseudometric on `set_val`. This now just a few easy instances. Then we define a mixin for...
##### Motivation for this change @LaurenceRideau ##### 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) #####...
https://github.com/math-comp/analysis/blob/d64e9df02884ed1a100efce56f07dd9b448fac7d/theories/lebesgue_measure.v#L1435
`Normedmodtype.v` is a long file, and this triggers several issues, alike the one descripe in [Issue#1167](https://github.com/math-comp/analysis/issues/1167) advocating the spit of `topology.v`. - Compilation takes a long time, when trying to...
Adding discrete topologies, uniformities, and metrics to the hierarchy. Cleans up a bunch of pre-HB issues, and now we can use `bool` directly instead of through a bunch of aliases....
The formalization of Baire and Banach-Steinhaus theorems (PR https://github.com/math-comp/analysis/pull/334) led to the introduction of the following definitions: ```coq bounded_fun_norm pointwise_bounded uniform_bounded ``` See commit https://github.com/math-comp/analysis/commit/3828a154f96d3027f09f7b9237203d59fd21f25e (note that it erroneously refers...
it appeared during the conversion of PR #1306 that we might like to have the following lemma: ```coq Lemma measurable_fun_indic_eqr D f g : measurable_fun D f -> measurable_fun D...
put the first part in a file `measurable_realfun.v`
```coq Lemma big_lexi_order_prefix_closed_itv {d} {K : nat -> tbOrderType d} n (x : big_lexi_order K) : same_prefix n x = `[ (@start_with K n x (fun=>\bot):big_lexi_order K)%O, (start_with n x...