Alessandro Bruni
Alessandro Bruni
Dear infotheo authors, I want to point out that my co-authors and I have a paper on the formalization of bounds on the trimmed mean algorithm that uses infotheo. It...
##### Motivation for this change Introduces probabilistic convergence ##### Things done/to do - [ ] add weak law of large numbers - [ ] prove Markov's and Chebyshev's inequality -...
We are missing the following: definition of multiplication of random variables and ring structure for RVs. ```coq Definition mul_RV (U : finType) (P : {fdist U}) (X Y : {RV...
This is used in mathcomp-analysis for defining probabilities, I think it would be generally helpful to have it
##### Motivation for this change I'm opening this draft PR to track the progress on this branch. The PR contributes a definition of Bernoulli trials and its central limit theorem....
##### Motivation for this change Introducing the Giry monad for probabilities, draft PR for now to track progress. ##### Checklist - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [...
https://github.com/math-comp/analysis/blob/c8adb03b2de691e9ed7def8bbd1028720ef918e4/theories/measure.v#L1829 The version using `\+` would be more useful, e.g.: ```coq Lemma measure_addE : measure_add = m1 \+ m2. Proof. by apply: funext=>A; rewrite /measure_add/= /msum 2!big_ord_recl/= big_ord0 adde0. Qed....
This would much improve the presentation of Minkowski's inequality and therefore PR #1000 Here is a draft by @affeldt-aist ```coq Section hoelder_conjugate. Context {R : realType}. Local Open Scope ereal_scope....
It would be good to automate testing with `meson`. Currently PR #72 contains an attempt at running one test as described in PR #71, which introduced `meson`.
Hi! I picked up on your first comment about testing functionality and I tried to setup a test with meson. Now if you run `meson test` in the build directory,...