analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
https://github.com/math-comp/analysis/blob/72c8678f8def77da4c1c2682f857cfb8cf770352/coq-mathcomp-analysis-stdlib.opam#L23 `Mathematics/Real Calculus and Topology` is maybe more appropriate see https://github.com/rocq-prover/opam/pull/3571#discussion_r2517233073
##### Motivation for this change This PR is based on PR #912 . It corresponds to the contents of the following paper: Reynald Affeldt, Yoshihiro Ishiguro, and Zachary Stone. Equational...
There is the notation `{within i, continuous f}` for an interval i and function f : R -> R where R : realType, but this notation `{within i, ...}` can...
https://github.com/math-comp/analysis/blob/86c655f6fa0a3db3f9638fff6da2ad39fb3937d6/Makefile.common#L121 ```text Warning: DEPRECATED: Use `-file-graph` Warning: DEPRECATED: Use `-structure-graph` ``` @yoshihiro503
See the following definition https://github.com/math-comp/analysis/blob/97d07798ab1fd1889ed707181c06cf98c438e408/theories/exp.v#L996-L1001 Note that for real numbers, the limit of the power function when the exponent is negative, goes to 0.
https://github.com/math-comp/analysis/blob/3b30884c4a9134f8c98cfab47c9cfa7f6fd4db0d/reals_stdlib/Rstruct.v#L551 as discussed in the conversation of PR https://github.com/math-comp/analysis/pull/1736 @t6s @CohenCyril
from the conversion of PR #1651 "Suggestions for future changes: We will not need to maintain two definitions of product measures as first-class; instead we can define the product measure...
```coq Lemma lebesgue_borel_int_eq (f : R -> \bar R) : measurable_fun (T := g_sigma_algebraType (R.-ocitv.-measurable)) setT f -> \int[lebesgue_measure]_x f x = \int[completed_lebesgue_measure]_x f x. ``` Is there a way...
##### Motivation for this change Introduces Hoeffding's inequality ##### Checklist - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding documentation in the headers Reference: [How to...
##### Motivation for this change Proof of Mertens theorems. This still requires a bit of prettyfiyng, but the proof is complete if someone wants to take a look. Dependecies: -...
