analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
##### Motivation for this change `integral_sum` was a missing lemma that we noticed when doing the `sampling` branch, this triggered a generation of `integrable_sum`, we do not use them in...
##### 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...
##### Motivation for this change closes draft PR #1613 @jmmarulang : I have duplicated your PR to avoid pushing on your master ##### Checklist - [x] added corresponding entries in...
fixes #1044 ##### Motivation for this change This PR demonstrates separation axioms. It defines the Sorgenfrey line and proves it totally disconnected. We intend to also prove that it is...
This PR contains the Bernoulli sampling theorem as described in the paper: ## Formalizing concentration inequalities in Rocq: infrastructure and automation by Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux,...
##### Motivation for this change When working on the `sampling` branch, we realized that we need variants of existing Fubini lemmas but adding these variants was no compatible with the...
##### Motivation for this change I added an alternative proof of gauss integral and placed it in theories/showcase. This is an experimental approach of improper integral. The difference of proof...
##### Motivation for this change the natural logarithm for the extended reals is needed for extending hoelder into the extended reals. ##### Checklist - [X] added corresponding entries in `CHANGELOG_UNRELEASED.md`...
What about renaming `derivemxE` to `deriveEjacobian` ? https://github.com/math-comp/analysis/blob/14c5bf819bce88100955bc655f0307568e13391c/theories/derive.v#L356 In my opinion, it is more appropriate because we can see by the name which alternative definition of directional derivative we're about...
https://github.com/math-comp/analysis/blob/c5ea0abfda9c1ec4f223ea2e013de20fbf23135f/theories/hoelder.v#L370 Lemmas relying on this specialization should be future proof for when the restriction on the argument of the norm is lifted, i.e., when this becomes `Local Notation "'N_ p...