math-comp
Add section: cdf of lebesgue stieltjes measure
Motivation for this change
I add Section cdf_of_lebesgue_stieltjes_mesure in probability.v, which proves that the cumulative distribution function of a Lebesgue-Stieltjes measure goes back to the underlying function.
Checklist
-
[x] added corresponding entries in
CHANGELOG_UNRELEASED.md -
[ ] added corresponding documentation in the headers
Reference: How to document
Merge policy
As a rule of thumb:
- PRs with several commits that make sense individually and that all compile are preferentially merged into master.
- PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers
- Read this Checklist
- Put a milestone if possible
- Check labels
This error is strange.
Error: The variable truncn was not found in the current environment.
Why was truncn not found? I can certainly find truncn in archimedean.v.
This error is strange.
Error: The variable truncn was not found in the current environment.Why was
truncnnot found? I can certainly findtruncnin archimedean.v.
It might be because the CI is testing with the previous version of MathComp (2.3.0) in which there was no truncn.
Thank you for the comment. Then I think the pull request went well, but please tell me if I need to fix something.
I have introduced a tentative structure Cumulative01 that carries the proofs that the function tends to 0 in -oo and to 1 in +oo. This way we can put the HB declaration that the Lebesgue-Stieltjes measure of such a function is a probability measure in lebesgue_stieltjes_measure.v and cdf_lebesgue_stieltjes_id still type-checks. (fyi: @CohenCyril )
TODO: write documentation and changelog for Cumulative01 if deemed useful.
@affeldt-aist Thank you very much for the review. I'd prefer to generalize 0 and 1, something like
HB.mixin Record isCumulativeBdd (R : numFieldType) (l u : R) (f : R -> R) := {
cumulativeNyl : f @ -oo --> (l:R) ;
cumulativeyu : f @ +oo --> (u:R) }.
#[short(type=cumulativeBdd)]
HB.structure Definition CumulativeBdd (R : numFieldType) (l u : R) :=
{ f of isCumulativeBdd R l u f & Cumulative R f}.
Arguments cumulativeNyl {R} l u s.
Arguments cumulativeyu {R} l u s.
Section probability_measure_of_lebesgue_stieltjes_mesure.
Context {R : realType} (f : @cumulativeBdd R 0 1).
But it's up to you, because 0 and 1 are sufficient for the time being.
If think that it is ok to merge since the work will anyway continue with issue https://github.com/math-comp/analysis/issues/1572 . @CohenCyril any thought?