analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
##### Motivation for this change Rewrite `fimfunE` so as to use fsbigop @CohenCyril ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` (do not edit former entries, only...
##### Motivation for this change happened to be the one I wanted for a proof ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` ~~- [ ] added...
##### Motivation for this change fixes #745 ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` ~~- [ ] added corresponding documentation in the headers~~ ##### Automatic note...
Co-authored-by: Takafumi Saikawa CO-authored-by: zstone1 ##### Motivation for this change Just to share the observation that the definition of exp called for extra type annotation `: complex_ringType _` ##### Things...
##### Motivation for this change ----- Overall goal ----- More cantor space helper theorems. The overall goal is to prove that, for countable `I`, `I -> C` is homeomorphic to...
Notations like `{within A, continuous f}` that specialize a common one (E.G. `continuous f`) don't print correctly. For a full list, `{within A, continuous f}` prints as `continuous f` `{...
##### Motivation for this change This PR provides a formalization of s-finite kernels with an application to probabilistic programs, this experiment is documented in this paper: https://inria.hal.science/hal-03917948/ This PR has...
The `\o` and `^-1` operation used in entourages are instances of a much more general "relation composition". We should add this notion to classical_sets, build its theory. There are several...
https://github.com/math-comp/analysis/blob/d2ef896b1120fc2ea8e0f1c7cfaa7a8df34ce8d8/theories/lebesgue_integral.v#L2074-L2075 Maybe this should be `ge0_integral_nnseries`.
The following code has an error (when "JustPath" is commented out). ``` (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrint...