Add section: cdf of lebesgue stieltjes measure

[Yosuke-Ito-345]

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

• 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

[Yosuke-Ito-345]

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.

[affeldt-aist]

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.

It might be because the CI is testing with the previous version of MathComp (2.3.0) in which there was no truncn.

[Yosuke-Ito-345]

Thank you for the comment.
Then I think the pull request went well, but please tell me if I need to fix something.

[Yosuke-Ito-345]

@affeldt-aist Would it be possible to review this pull request?

[affeldt-aist]

I think it is fine.
Maybe the declaration of lebesgue_stieltjes_measure as a probability measure should move to the file where the Lebesgue Stieltjes measure is defined, let's try before merging.

[affeldt-aist]

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.

[Yosuke-Ito-345]

@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.

[affeldt-aist]

If think that it is ok to merge since the work will anyway continue with issue #1572 . @CohenCyril any thought?

[Yosuke-Ito-345]

Thank you for the review and the merge.